agentleFS
Sign inStart free
rainoftimerainoftime/pl-skills/axiomatic-semantics/SKILL.md

axiomatic-semantics

Skill17 starsChanged 9 months agoApache-2.0View on GitHub

Define program meaning through logical assertions and proof rules (Hoare logic).

The file

We split this skill into the rules it gives an agent

7 rules. About 0 are common, 7 are distinctive, and 0 are very specific to this project.

  • ≈0

    Common · estimate

    Many files like this have a rule of this kind.

  • ≈7

    Distinctive · estimate

    This author's own choices. Worth a look.

  • 0

    Very specific

    Tied to their project's names, files or tools. Probably skip.

  • Common
  • Distinctive
  • Very specific
  1. Distinctive:

    Start with the postcondition, work backwards

    line 43
  2. Distinctive:

    Use Z3 or other SMT solvers for implication checking

    line 45
  3. Distinctive:

    When operational semantics suffices

    line 84
  4. Distinctive:

    When automation is required (use model checking)

    line 86
  5. Distinctive:

    No built-in concurrency reasoning (see separation logic)

    line 92
  6. Distinctive:

    Solution: Every rule now includes explicit frame conditions.

    line 174
  7. Distinctive:

    Test generation supplements invariant inference

    line 181

≈ “Common” is an estimate: at least 1 in 5 of the 350,495 skill files we read have a rule of the same kind, not the same words. “Very specific” is our guess from the words: it names a file, a command, a setting or the project itself.

Keep what fits and drop the rest. Your version, ready for your agents.
Files
SKILL.md

Axiomatic Semantics

Axiomatic semantics defines program meaning through logical assertions about program states. Hoare logic, the primary framework, uses triples {P} C {Q} meaning "if P holds before C, then Q holds after C terminates."

When to Use This Skill

  • Verifying program correctness
  • Designing proof systems
  • Teaching formal verification
  • Specifying program behavior
  • Building verification tools

What This Skill Does

  1. Assertion Language: Define predicates over program states
  2. Hoare Triples: Specify pre/post conditions
  3. Proof Rules: Derive correctness properties
  4. Weakest Precondition: Compute necessary preconditions
  5. Loop Invariants: Handle iteration constructs

Key Concepts

ConceptDescription
Hoare Triple{P} C {Q} - precondition, command, postcondition
Weakest PreconditionLargest set of states guaranteeing Q after C
Loop InvariantProperty holding before, during, and after loop
Partial CorrectnessIf terminates, postcondition holds
Total CorrectnessTerminates and postcondition holds

Tips

  • Start with the postcondition, work backwards
  • Find good loop invariants (the hard part)
  • Use Z3 or other SMT solvers for implication checking
  • Annotate loops with invariants explicitly
  • Total correctness requires termination proofs

Common Use Cases

  • Verifying algorithm correctness
  • Security proofs
  • Compiler correctness
  • Teaching formal methods
  • Specification languages (JML, ACSL)

Related Skills

  • hoare-logic-verifier - Verification tool
  • separation-logician - Memory reasoning
  • smt-solver-interface - Automated proving
  • operational-semantics-definer - Operational view

Canonical References

ReferenceWhy It Matters
Hoare, "An Axiomatic Basis for Computer Programming" (CACM 1969)Original Hoare logic (Turing Award)
Dijkstra, "A Discipline of Programming" (1976)Weakest preconditions
Winskel, "The Formal Semantics of Programming Languages" (1993)Comprehensive treatment

Tradeoffs and Limitations

Approach Tradeoffs

ApproachProsCons
Hoare LogicCompositional, intuitiveNeed loop invariants
Weakest PreconditionAutomatic derivationComplex expressions
Strongest PostconditionForward reasoningLess compositional

When NOT to Use This Skill

  • When operational semantics suffices
  • For non-terminating programs (partial vs total)
  • When automation is required (use model checking)

Limitations

  • Undecidable in general
  • Requires loop invariant annotations
  • No built-in concurrency reasoning (see separation logic)

Assessment Criteria

A high-quality implementation should have:

CriterionWhat to Look For
SoundnessProven triples are actually valid
CompletenessValid triples can be proven
AutomationUses SMT solver for implications
ExpressivenessHandles loops, procedures

Quality Indicators

✅ Good: Sound proof rules, handles loops, SMT integration ⚠️ Warning: Manual invariant annotation required ❌ Bad: Unsound rules, no loop support

Research Tools & Artifacts

Real-world axiomatic semantics tools to study:

ToolWhy It Matters
VerifastVerified C programs with separation logic
Frama-C (WP)Industrial-strength C verification
Why3Platform for deductive verification
OpenJMLJava bytecode verification with JML
ViperVerification framework with permission reasoning
ACSL (Frama-C)ANSI/ISO C Specification Language

Key Verification Systems

  • Dafny: Verifiable programs with inline proofs
  • F* : Effectful verification with meta-theory
  • Coq: Interactive proof with extraction to verified code
  • Isabelle/HOL: Generic proof assistant

Research Frontiers

Current active research in axiomatic semantics:

DirectionKey PapersChallenge
Automation"From Hoare Logic to Separation Logic" (2018)Auto-generating loop invariants
Fractional permissions"Fractional Permissions" (2010)Concurrent read/write sharing
Concurrent separation logicO'Hearn, Brookes "Resources, Concurrency and Local Reasoning" (2004/2007)Verifying lock-free algorithms
Iris"Higher-Order Ghost State" (2015)Complex concurrency patterns
Relational verificationBenton "Simple Relational Correctness Proofs" (2004)Proving equivalence of programs

Hot Topics

  1. SMT integration: Better theory support for arithmetic
  2. Horn clauses: Automatic invariant generation
  3. Learning-based invariants: Using ML to suggest invariants
  4. Quantum Hoare logic: Verification for quantum programs

Implementation Pitfalls

Common bugs in verification tools:

PitfallReal ExamplePrevention
Missing frame ruleFrama-C early versionsExplicit frame conditions
Unsound loop invariantESC/Java missing measuresCheck variant/measure
Weak memoryVerifiers assuming sequentialModel weak memory explicitly
Arithmetic overflowACL2 unsoundness caseBounded arithmetic support
Aliasing bugsMissing permission checksAlways track permissions
Incomplete theoriesMissing bitvector supportCover all language features

The "Frame Rule" Bug

Early separation logic verifiers forgot the frame rule:

// @requires P
// @ensures P * Q
void foo() {
    // Could lose Q if not framed!
}

Solution: Every rule now includes explicit frame conditions.

Automation vs. Expressiveness Tradeoff

The core tension: more automation → less expressiveness:

  • Full separation logic is undecidable
  • Bi-abduction finds frame automatically (DISEL, etc.)
  • Test generation supplements invariant inference

Download now (ZIP)

Does it work?

Reviews from people and from AI agents that ran it: what they used it for, and whether it worked.

Reviews can't be read right now.

Your trail

Files you open will collect here, so you can find them again.

Open two or more, and you can remix the rules you like from each into one list. Kept in this browser only.

Now do this for your own.

Bring your CLAUDE.md, AGENTS.md or skills. agentleFS shows which of your rules are common, which are yours and which only fit one project, and keeps one version your agents read everywhere.

Check your setup, free