Partial correctness and loop invariants for PDL

17 fully proved

PDL

DefinitionPartial-correctness Hoare triple for PDL programs#✓fully proved

Every execution of a from P ends in Q, without a termination requirement.

def Hoare (M : Model World Atom Label) (P : Set World)
    (a : Program Atom Label) (Q : Set World) : Prop :=
  ∀ ⦃s t⦄, s ∈ P → ProgRel M a s t → t ∈ Q

Uses 3 · Used by 14

Statement usesPDL model · Relation denoted by a PDL program · PDL programs

Used byHoare rule for nondeterministic choice · Hoare rule of consequence · Hoare triples with formula assertions as box validity · Partial correctness as inclusion in the relational core · Hoare triples as KAT absorption equations · Hoare triples as KAT test inequalities · Hoare rule for sequential composition · Hoare invariant rule for iteration · Hoare rule for formula tests · Test absorption lifts through iteration · Loop exit absorption from a guarded-body absorption equation · Hoare invariant rule for guarded while loops · While-loop rule with initialization and exit implication · Semantic completeness of the while-loop invariant rule

TheoremPartial correctness as inclusion in the relational core#✓fully proved

Partial correctness agrees with the canonical relation's core.

theorem hoare_iff_subset_core :
    Hoare M P a Q ↔ P ⊆ SetRel.core (a.toRelation M) Q

Uses 5 · Used by 2

Statement usesPartial-correctness Hoare triple for PDL programs · PDL model · PDL programs · Relational interpretation of a PDL program

Proof usesRelation denoted by a PDL program

Used byHoare triples as KAT absorption equations · Hoare triples as KAT test inequalities

TheoremHoare triples as KAT test inequalities#✓fully proved

Hoare verification is equivalent to the KAT test inequality.

theorem hoare_iff_test_le :
    Hoare M P a Q ↔ testSet P * a.toRelation M ≤
      a.toRelation M * testSet Q

Uses 7

Statement usesPartial-correctness Hoare triple for PDL programs · PDL model · PDL programs · Relational interpretation of a PDL program · Diagonal test relation of an assertion

Proof usesPartial correctness as inclusion in the relational core · Verification inequality characterizes partial correctness

TheoremHoare triples as KAT absorption equations#✓fully proved

The equivalent KAT absorption equation for verification.

theorem hoare_iff_test_eq :
    Hoare M P a Q ↔ testSet P * a.toRelation M =
      testSet P * a.toRelation M * testSet Q

Uses 7 · Used by 2

Statement usesPartial-correctness Hoare triple for PDL programs · PDL model · PDL programs · Relational interpretation of a PDL program · Diagonal test relation of an assertion

Proof usesPartial correctness as inclusion in the relational core · Postcondition absorption characterizes partial correctness

Used byTest absorption lifts through iteration · Loop exit absorption from a guarded-body absorption equation

TheoremHoare triples with formula assertions as box validity#✓fully proved

Formula assertions connect Hoare verification to global PDL validity, not just an atomic-action modality.

theorem hoare_iff_box (φ ψ : Formula Atom Label) :
    Hoare M {s | Sat M φ s} a {s | Sat M ψ s} ↔
      ∀ s, Sat M (.imp φ (.box a ψ)) s

Uses 6

Statement usesPDL formulas · Partial-correctness Hoare triple for PDL programs · PDL model · PDL programs · Satisfaction of PDL formulas

Proof usesRelation denoted by a PDL program

Hoare

TheoremHoare rule of consequence#✓fully proved

Strengthen the precondition and weaken the postcondition.

theorem consequence {P' Q' : Set World} (h : Hoare M P a Q)
    (hP : P' ⊆ P) (hQ : Q ⊆ Q') : Hoare M P' a Q'

Uses 4 · Used by 1

Statement usesPartial-correctness Hoare triple for PDL programs · PDL model · PDL programs

Proof usesRelation denoted by a PDL program

Used byWhile-loop rule with initialization and exit implication

TheoremHoare rule for sequential composition#✓fully proved

Sequential verification uses the first postcondition as the second precondition.

theorem seq (ha : Hoare M P a I) (hb : Hoare M I b Q) :
    Hoare M P (.seq a b) Q

Uses 4

Statement usesPartial-correctness Hoare triple for PDL programs · PDL model · PDL programs

Proof usesRelation denoted by a PDL program

TheoremHoare rule for nondeterministic choice#✓fully proved

Nondeterministic choice is safe exactly when both branches are.

theorem choice_iff :
    Hoare M P (.choice a b) Q ↔ Hoare M P a Q ∧ Hoare M P b Q

Uses 4

Statement usesPartial-correctness Hoare triple for PDL programs · PDL model · PDL programs

Proof usesRelation denoted by a PDL program

TheoremHoare rule for formula tests#✓fully proved

A formula test requires the postcondition only where the test passes.

theorem test_iff (φ : Formula Atom Label) :
    Hoare M P (.test φ) Q ↔ P ∩ {s | Sat M φ s} ⊆ Q

Uses 6

Statement usesPDL formulas · Partial-correctness Hoare triple for PDL programs · PDL model · PDL programs · Satisfaction of PDL formulas

Proof usesRelation denoted by a PDL program

TheoremHoare invariant rule for iteration#✓fully proved

A one-step invariant holds after every finite number of iterations, including zero, via CSLib's canonical closure-preservation theorem.

theorem star (h : Hoare M I a I) : Hoare M I (.star a) I

Uses 4 · Used by 2

Statement usesPartial-correctness Hoare triple for PDL programs · PDL model · PDL programs

Proof usesRelation denoted by a PDL program

Used byTest absorption lifts through iteration · Hoare invariant rule for guarded while loops

PDL

DefinitionGuarded while loop in PDL#✓fully proved

A guarded loop in the existing PDL syntax: iterate guarded body steps, then test that the guard is false.

def Program.whileDo (guard : Formula Atom Label)
    (body : Program Atom Label) : Program Atom Label :=
  .seq (.star (.seq (.test guard) body)) (.test (.imp guard .bot))

Uses 2 · Used by 4

Statement usesPDL formulas · PDL programs

Used byLoop exit absorption from a guarded-body absorption equation · Hoare invariant rule for guarded while loops · While-loop rule with initialization and exit implication · Semantic completeness of the while-loop invariant rule

Hoare

TheoremHoare invariant rule for guarded while loops#✓fully proved

The guarded-loop invariant rule is partial correctness, including zero-step exits; it does not guarantee termination.

theorem whileDo (guard : Formula Atom Label)
    (h : Hoare M (I ∩ {s | Sat M guard s}) a I) :
    Hoare M I (Program.whileDo guard a) (I ∩ {s | ¬ Sat M guard s})

Uses 8 · Used by 2

Statement usesPDL formulas · Partial-correctness Hoare triple for PDL programs · PDL model · PDL programs · Guarded while loop in PDL · Satisfaction of PDL formulas

Proof usesHoare invariant rule for iteration · Relation denoted by a PDL program

Used byLoop exit absorption from a guarded-body absorption equation · While-loop rule with initialization and exit implication

TheoremWhile-loop rule with initialization and exit implication#✓fully proved

Verify a guarded loop using initialization, invariant preservation, and the exit implication to the desired postcondition.

theorem whileDo_consequence (guard : Formula Atom Label)
    (hinit : P ⊆ I) (hbody : Hoare M (I ∩ {s | Sat M guard s}) a I)
    (hexit : I ∩ {s | ¬ Sat M guard s} ⊆ Q) :
    Hoare M P (Program.whileDo guard a) Q

Uses 8 · Used by 1

Statement usesPDL formulas · Partial-correctness Hoare triple for PDL programs · PDL model · PDL programs · Guarded while loop in PDL · Satisfaction of PDL formulas

Proof usesHoare rule of consequence · Hoare invariant rule for guarded while loops

Used bySemantic completeness of the while-loop invariant rule

TheoremSemantic completeness of the while-loop invariant rule#✓fully proved

The guarded-loop rule is semantically complete for arbitrary set assertions. The witness is guarded-body reachability from P, independent of Q; this is not a completeness claim for a syntactic assertion language.

theorem whileDo_iff_exists_invariant (guard : Formula Atom Label) :
    Hoare M P (Program.whileDo guard a) Q ↔
      ∃ I : Set World, P ⊆ I ∧
        Hoare M (I ∩ {s | Sat M guard s}) a I ∧
        I ∩ {s | ¬ Sat M guard s} ⊆ Q

Uses 9

Statement usesPDL formulas · Partial-correctness Hoare triple for PDL programs · PDL model · PDL programs · Guarded while loop in PDL · Satisfaction of PDL formulas

Proof usesWhile-loop rule with initialization and exit implication · Relation denoted by a PDL program · Relational interpretation of a PDL program

PDL

TheoremPDL induction restricted to reachable states#✓fully proved

PDL induction restricted to states reachable from the initial world. This proves [a*](φ → [a]φ) → (φ → [a*]φ) without assuming preservation on unreachable states.

theorem sat_box_star_induction {φ : Formula Atom Label} {s : World}
    (hstep : Sat M (.box (.star a) (.imp φ (.box a φ))) s)
    (hinit : Sat M φ s) : Sat M (.box (.star a) φ) s

Uses 5

Statement usesPDL formulas · PDL model · PDL programs · Satisfaction of PDL formulas

Proof usesRelation denoted by a PDL program

TheoremTest absorption lifts through iteration#✓fully proved

Concrete relational test absorption lifts through PDL iteration, connecting the algebraic verification equation to closure invariance.

theorem test_mul_star_absorption
    (h : testSet I * a.toRelation M =
      testSet I * a.toRelation M * testSet I) :
    testSet I * a.star.toRelation M =
      testSet I * a.star.toRelation M * testSet I

Uses 7

Statement usesPDL model · PDL programs · Relational interpretation of a PDL program · Diagonal test relation of an assertion

Proof usesPartial-correctness Hoare triple for PDL programs · Hoare invariant rule for iteration · Hoare triples as KAT absorption equations

TheoremLoop exit absorption from a guarded-body absorption equation#✓fully proved

A guarded-body verification equation implies the loop's exit verification equation over the same canonical relational carrier.

theorem test_mul_whileDo_absorption (guard : Formula Atom Label)
    (h : testSet (I ∩ {s | Sat M guard s}) * a.toRelation M =
      testSet (I ∩ {s | Sat M guard s}) * a.toRelation M * testSet I) :
    testSet I * (Program.whileDo guard a).toRelation M =
      testSet I * (Program.whileDo guard a).toRelation M *
        testSet (I ∩ {s | ¬ Sat M guard s})

Uses 10

Statement usesPDL formulas · PDL model · PDL programs · Relational interpretation of a PDL program · Guarded while loop in PDL · Satisfaction of PDL formulas · Diagonal test relation of an assertion

Proof usesPartial-correctness Hoare triple for PDL programs · Hoare invariant rule for guarded while loops · Hoare triples as KAT absorption equations

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.