Hoare logic

AbbreviationAssertion#✓fully proved

An assertion is a predicate on program states: it assigns a proposition to each state. Assertions serve as the preconditions and postconditions of Hoare triples.

abbrev Assertion := State → Prop
Uses 1 · Used by 44
Statement usesIMP program states
Used byRelative completeness of total-correctness Hoare logic · Total-correctness Hoare logic is relatively complete · Derivability in Hoare logic for partial correctness · Total-correctness derivations give partial-correctness derivations · Partial-correctness Hoare logic matches the denotational semantics · Partial-correctness Hoare logic as an inference system · Derivability in the default inference system on Hoare triples is validity · Total-correctness Hoare logic as an inference system · The weakest liberal precondition gives a derivable triple · Entailment of assertions · Loop invariants entail the weakest liberal precondition of the loop · Total-correctness weakest precondition implies the weakest liberal precondition · Soundness of Hoare logic for partial correctness · Soundness of total-correctness Hoare logic · Precondition strengthening for partial correctness · Precondition strengthening for total correctness · Substitution in an assertion · Total-correctness Hoare logic · Total-correctness Hoare logic is sound and complete for the denotational semantics · Soundness and relative completeness of total-correctness Hoare logic · The weakest-precondition triple is derivable in total-correctness Hoare logic · Total correctness gives a terminating small-step run · Hoare triples · Validity of total-correctness Hoare triples · Validity of a Hoare triple · Total correctness implies partial correctness · Weakest-precondition unfolding of a while loop · Invariant rule for while loops · Weakest liberal precondition unfolding of a while loop · Variant rule for while loops · Weakest liberal precondition · Weakest precondition for total correctness · Hoare validity embeds into separation validity · Framed embedding of Hoare validity · Annotated commands · Precondition of an annotated command · Weakening the postcondition of an annotated command · Erasing annotations · Verification condition of an annotated command · Completeness of verification conditions for derivable triples · Completeness of verification conditions for valid triples · Soundness of verification conditions · Verification conditions yield valid Hoare triples · Hoare validity via small-step termination

DefinitionEntailment of assertions#✓fully proved

An assertion \(P\) entails an assertion \(Q\) when every state that satisfies \(P\) also satisfies \(Q\).

def Entails (left right : Assertion) : Prop :=
  ∀ ⦃state⦄, left state → right state
Uses 2 · Used by 16
Statement usesAssertion · IMP program states
Used byRelative completeness of total-correctness Hoare logic · Total-correctness Hoare logic is relatively complete · Derivability in Hoare logic for partial correctness · The weakest liberal precondition gives a derivable triple · Loop invariants entail the weakest liberal precondition of the loop · Soundness of Hoare logic for partial correctness · Soundness of total-correctness Hoare logic · Precondition strengthening for partial correctness · Precondition strengthening for total correctness · Total-correctness Hoare logic · The weakest-precondition triple is derivable in total-correctness Hoare logic · Weakening the postcondition of an annotated command · Completeness of verification conditions for derivable triples · Completeness of verification conditions for valid triples · Soundness of verification conditions · Verification conditions yield valid Hoare triples

DefinitionSubstitution in an assertion#✓fully proved

Let \(P\) be an assertion, \(x\) a variable and \(e\) an arithmetic expression. The assertion \(P[e/x]\) holds in a state \(s\) exactly when \(P\) holds in the state obtained from \(s\) by setting the value of \(x\) to the value of \(e\) in \(s\).

def subst (post : Assertion) (name : Nat) (value : AExp) : Assertion :=
  fun state => post (Function.update state name (value.eval state))
Uses 4 · Used by 9
Statement usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Assertion · IMP program states
Used byDerivability in Hoare logic for partial correctness · The weakest liberal precondition gives a derivable triple · Soundness of Hoare logic for partial correctness · Soundness of total-correctness Hoare logic · Total-correctness Hoare logic · The weakest-precondition triple is derivable in total-correctness Hoare logic · Precondition of an annotated command · Completeness of verification conditions for derivable triples · Soundness of verification conditions

DefinitionValidity of a Hoare triple#✓fully proved

For assertions \(P\) and \(Q\) and a command \(c\), the partial-correctness Hoare triple \(\lbrace P \rbrace\ c\ \lbrace Q \rbrace\) is valid when, for all states \(s\) and \(t\), if \(s\) satisfies \(P\) and executing \(c\) from \(s\) terminates in \(t\) under the big-step semantics, then \(t\) satisfies \(Q\).

def Valid (pre : Assertion) (command : Cmd) (post : Assertion) : Prop :=
  ∀ ⦃initial final⦄, pre initial → BigStep command initial final → post final
Uses 4 · Used by 13
Statement usesAssertion · Big-step semantics of IMP · Commands of IMP · IMP program states
Used byRelative completeness of total-correctness Hoare logic · Partial-correctness Hoare logic matches the denotational semantics · Partial-correctness Hoare logic as an inference system · Derivability in the default inference system on Hoare triples is validity · Loop invariants entail the weakest liberal precondition of the loop · Soundness of Hoare logic for partial correctness · Total correctness implies partial correctness · Invariant rule for while loops · Hoare validity embeds into separation validity · Framed embedding of Hoare validity · Completeness of verification conditions for valid triples · Verification conditions yield valid Hoare triples · Hoare validity via small-step termination

TheoremInvariant rule for while loops#✓fully proved

Let \(I\) be an assertion, \(b\) a Boolean expression and \(c\) a command. Write \(I \wedge b\) for the assertion that \(I\) holds and \(b\) evaluates to true, and \(I \wedge \neg b\) for the assertion that \(I\) holds and \(b\) evaluates to false. If the partial-correctness Hoare triple \(\lbrace I \wedge b \rbrace\ c\ \lbrace I \rbrace\) is valid, then so is the triple \(\lbrace I \rbrace\ \mathtt{while}\ b\ \mathtt{do}\ c\ \lbrace I \wedge \neg b \rbrace\).

theorem whileLoop {invariant : Assertion} {guard : BExp} {body : Cmd}
    (hbody : Valid (fun state => invariant state ∧ guard.eval state = true)
      body invariant) :
    Valid invariant (.while guard body)
      (fun state => invariant state ∧ guard.eval state = false)
Uses 9 · Used by 2
Statement usesAssertion · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Commands of IMP · IMP program states · Validity of a Hoare triple
Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Big-step semantics of IMP
Used byLoop invariants entail the weakest liberal precondition of the loop · Soundness of Hoare logic for partial correctness

DefinitionWeakest liberal precondition#✓fully proved

For a command \(c\) and an assertion \(Q\), the weakest liberal precondition of \(c\) with respect to \(Q\) is the assertion that holds in a state \(s\) exactly when every state \(t\) in which an execution of \(c\) from \(s\) terminates, under the big-step semantics, satisfies \(Q\).

It is liberal because no termination claim is made: a state from which \(c\) has no terminating execution satisfies it for every \(Q\).

def wlp (command : Cmd) (post : Assertion) : Assertion :=
  fun initial => ∀ ⦃final⦄, BigStep command initial final → post final
Uses 4 · Used by 5
Statement usesAssertion · Big-step semantics of IMP · Commands of IMP · IMP program states
Used byRelative completeness of total-correctness Hoare logic · The weakest liberal precondition gives a derivable triple · Loop invariants entail the weakest liberal precondition of the loop · Total-correctness weakest precondition implies the weakest liberal precondition · Weakest liberal precondition unfolding of a while loop

TheoremWeakest liberal precondition unfolding of a while loop#✓fully proved

Let \(b\) be a Boolean expression, \(c\) a command and \(Q\) an assertion. Write \(\mathrm{wlp}(d, R)\) for the weakest liberal precondition of a command \(d\) with respect to an assertion \(R\), and let \(W\) be the loop \(\mathbf{while}\ b\ \mathbf{do}\ c\). Then \(\mathrm{wlp}(W, Q)\) is the assertion that holds in a state \(s\) exactly when both of the following hold: if \(b\) evaluates to false in \(s\), then \(Q\) holds in \(s\); and if \(b\) evaluates to true in \(s\), then \(\mathrm{wlp}(c, \mathrm{wlp}(W, Q))\) holds in \(s\).

theorem whileLoop (guard : BExp) (body : Cmd) (post : Assertion) :
    wlp (.while guard body) post = fun state =>
      (guard.eval state = false → post state) ∧
      (guard.eval state = true → wlp body (wlp (.while guard body) post) state)
Uses 9 · Used by 1
Statement usesAssertion · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Commands of IMP · IMP program states · Weakest liberal precondition
Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Big-step semantics of IMP
Used byThe weakest liberal precondition gives a derivable triple

TheoremLoop invariants entail the weakest liberal precondition of the loop#✓fully proved

Let \(I\) and \(Q\) be assertions, \(b\) a Boolean expression and \(c\) a command. Suppose that every state satisfying \(I\) in which \(b\) evaluates to true satisfies the weakest liberal precondition of \(c\) with respect to \(I\), and that every state satisfying \(I\) in which \(b\) evaluates to false satisfies \(Q\). Then \(I\) entails the weakest liberal precondition of the loop \(\mathtt{while}\ b\ \mathtt{do}\ c\) with respect to \(Q\).

theorem invariant_le_while {invariant post : Assertion} {guard : BExp} {body : Cmd}
    (hbody : Assertion.Entails
      (fun state => invariant state ∧ guard.eval state = true) (wlp body invariant))
    (hexit : Assertion.Entails
      (fun state => invariant state ∧ guard.eval state = false) post) :
    invariant.Entails (wlp (.while guard body) post)
Uses 10
Statement usesAssertion · Entailment of assertions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Commands of IMP · IMP program states · Weakest liberal precondition
Proof usesBig-step semantics of IMP · Validity of a Hoare triple · Invariant rule for while loops

DefinitionValidity of total-correctness Hoare triples#✓fully proved

For assertions \(P\) and \(Q\) on states and a command \(c\), the total-correctness Hoare triple with precondition \(P\), command \(c\) and postcondition \(Q\) is valid when every state \(s\) satisfying \(P\) has a terminating big-step execution of \(c\) from \(s\) ending in a state \(t\) that satisfies \(Q\).

def TValid (pre : Assertion) (command : Cmd) (post : Assertion) : Prop :=
  ∀ ⦃s : State⦄, pre s → ∃ s', BigStep command s s' ∧ post s'
Uses 4 · Used by 8
Statement usesAssertion · Big-step semantics of IMP · Commands of IMP · IMP program states
Used byTotal-correctness Hoare logic is relatively complete · Total-correctness Hoare logic as an inference system · Soundness of total-correctness Hoare logic · Total-correctness Hoare logic is sound and complete for the denotational semantics · Soundness and relative completeness of total-correctness Hoare logic · Total correctness gives a terminating small-step run · Total correctness implies partial correctness · Variant rule for while loops

TheoremVariant rule for while loops#✓fully proved

Let \(I\) be an assertion (the invariant), \(V\) a function from states to natural numbers (the variant), \(b\) a Boolean guard and \(c\) a command. Suppose that for every state \(s\) satisfying \(I\) in which \(b\) evaluates to true, there is a terminating big-step execution of \(c\) from \(s\) ending in a state \(s'\) that satisfies \(I\) with \(V(s') < V(s)\). Then the total-correctness Hoare triple with precondition \(I\), command \(\mathtt{while}\ b\ \mathtt{do}\ c\) and postcondition "\(I\) holds and \(b\) evaluates to false" is valid.

theorem whileVariant {invariant : Assertion} {variant : State → Nat}
    {guard : BExp} {body : Cmd}
    (hbody : ∀ s, invariant s → guard.eval s = true →
      ∃ s', BigStep body s s' ∧ invariant s' ∧ variant s' < variant s) :
    TValid invariant (.while guard body)
      (fun s => invariant s ∧ guard.eval s = false)
Uses 7 · Used by 1
Statement usesAssertion · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Big-step semantics of IMP · Commands of IMP · IMP program states · Validity of total-correctness Hoare triples
Used bySoundness of total-correctness Hoare logic

TheoremTotal correctness implies partial correctness#✓fully proved

For assertions \(P\), \(Q\) and a command \(c\), if the total-correctness Hoare triple with precondition \(P\), command \(c\) and postcondition \(Q\) is valid, then the partial-correctness Hoare triple with the same precondition, command and postcondition is valid.

theorem valid {pre post : Assertion} {command : Cmd}
    (htotal : TValid pre command post) : Valid pre command post
Uses 7 · Used by 1
Statement usesAssertion · Commands of IMP · Validity of total-correctness Hoare triples · Validity of a Hoare triple
Proof usesBig-step semantics of IMP · Determinism of IMP big-step semantics · IMP program states
Used byTotal-correctness derivations give partial-correctness derivations

TheoremTotal correctness gives a terminating small-step run#✓fully proved

If the total-correctness Hoare triple with precondition \(P\), command \(c\) and postcondition \(Q\) is valid and a state \(s\) satisfies \(P\), then there is a state \(t\) such that \(c\), started in \(s\), reaches \(\mathtt{skip}\) with state \(t\) in finitely many small steps, and \(t\) satisfies \(Q\).

theorem terminates {pre post : Assertion} {command : Cmd}
    (htotal : TValid pre command post) {state : State} (hpre : pre state) :
    ∃ final, Terminates command state final ∧ post final
Uses 7
Statement usesAssertion · Commands of IMP · IMP program states · Validity of total-correctness Hoare triples · Termination of an IMP command
Proof usesBig-step semantics of IMP · Equivalence of small-step and big-step semantics

DefinitionWeakest precondition for total correctness#✓fully proved

For a command \(c\) and a postcondition \(Q\), the weakest precondition \(\mathrm{wp}(c, Q)\) is the assertion that holds at a state \(s\) exactly when there is a terminating big-step execution of \(c\) from \(s\) ending in a state that satisfies \(Q\).

def wp (command : Cmd) (post : Assertion) : Assertion :=
  fun s => ∃ s', BigStep command s s' ∧ post s'
Uses 4 · Used by 4
Statement usesAssertion · Big-step semantics of IMP · Commands of IMP · IMP program states
Used byTotal-correctness Hoare logic is relatively complete · Total-correctness weakest precondition implies the weakest liberal precondition · The weakest-precondition triple is derivable in total-correctness Hoare logic · Weakest-precondition unfolding of a while loop

TheoremWeakest-precondition unfolding of a while loop#✓fully proved

For a Boolean guard \(b\), a loop body \(c\), a postcondition \(Q\) and a state \(s\), the state \(s\) satisfies the total-correctness weakest precondition \(\mathrm{wp}(\mathtt{while}\ b\ \mathtt{do}\ c, Q)\) if and only if either \(b\) evaluates to false in \(s\) and \(s\) satisfies \(Q\), or \(b\) evaluates to true in \(s\) and \(s\) satisfies \(\mathrm{wp}(c, \mathrm{wp}(\mathtt{while}\ b\ \mathtt{do}\ c, Q))\).

theorem while_iff {guard : BExp} {body : Cmd} {post : Assertion}
    {state : State} :
    wp (.while guard body) post state ↔
      (guard.eval state = false ∧ post state) ∨
      (guard.eval state = true ∧
        wp body (wp (.while guard body) post) state)
Uses 9
Statement usesAssertion · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Commands of IMP · IMP program states · Weakest precondition for total correctness
Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Big-step semantics of IMP

TheoremTotal-correctness weakest precondition implies the weakest liberal precondition#✓fully proved

For every command \(c\), postcondition \(Q\) and state \(s\), if \(s\) satisfies the total-correctness weakest precondition \(\mathrm{wp}(c, Q)\), then \(s\) satisfies the weakest liberal precondition \(\mathrm{wlp}(c, Q)\).

theorem le_wlp {command : Cmd} {post : Assertion} {state : State}
    (hwp : wp command post state) : wlp command post state
Uses 7
Statement usesAssertion · Commands of IMP · IMP program states · Weakest liberal precondition · Weakest precondition for total correctness
Proof usesBig-step semantics of IMP · Determinism of IMP big-step semantics

InductiveDerivability in Hoare logic for partial correctness#✓fully proved

Here an assertion is a predicate on states, and an assertion \(P\) entails an assertion \(P'\) when every state satisfying \(P\) satisfies \(P'\). For an assertion \(P\) and a Boolean expression \(b\), the assertion \(P \land b\) holds in a state when \(P\) holds there and \(b\) evaluates to true in it, and the assertion \(P \land \lnot b\) holds in a state when \(P\) holds there and \(b\) evaluates to false in it. Derivability of partial-correctness Hoare triples \(\{P\}\,c\,\{Q\}\) is the least relation closed under the following rules, where \(P\), \(P'\), \(Q\), \(Q'\), \(R\) and \(I\) are assertions, \(c\), \(c_1\) and \(c_2\) are commands, \(x\) is a variable, \(a\) is an arithmetic expression and \(b\) is a Boolean expression.

  • Skip: \(\{Q\}\,\mathtt{skip}\,\{Q\}\).
  • Assignment: \(\{Q[a/x]\}\,x := a\,\{Q\}\), where \(Q[a/x]\) holds in a state \(s\) when \(Q\) holds in the state obtained from \(s\) by setting \(x\) to the value of \(a\) in \(s\).
  • Sequencing: from \(\{P\}\,c_1\,\{R\}\) and \(\{R\}\,c_2\,\{Q\}\) derive \(\{P\}\,c_1; c_2\,\{Q\}\).
  • Conditional: from \(\{P \land b\}\,c_1\,\{Q\}\) and \(\{P \land \lnot b\}\,c_2\,\{Q\}\) derive \(\{P\}\,\mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2\,\{Q\}\).
  • While: from \(\{I \land b\}\,c\,\{I\}\) derive \(\{I\}\,\mathtt{while}\ b\ \mathtt{do}\ c\,\{I \land \lnot b\}\).
  • Consequence: if \(P\) entails \(P'\), \(\{P'\}\,c\,\{Q'\}\) is derivable and \(Q'\) entails \(Q\), then \(\{P\}\,c\,\{Q\}\) is derivable.
Cslib.IMP.Derivable · 22 lines 
inductive Derivable : Assertion → Cmd → Assertion → Prop
  | skip (post : Assertion) : Derivable post .skip post
  | assign (post : Assertion) (name : Nat) (value : AExp) :
      Derivable (post.subst name value) (.assign name value) post
  | seq {pre middle post : Assertion} {first second : Cmd}
      (hfirst : Derivable pre first middle) (hsecond : Derivable middle second post) :
      Derivable pre (.seq first second) post
  | ite {pre post : Assertion} {guard : BExp} {thenBranch elseBranch : Cmd}
      (hthen : Derivable (fun state => pre state ∧ guard.eval state = true)
        thenBranch post)
      (helse : Derivable (fun state => pre state ∧ guard.eval state = false)
        elseBranch post) :
      Derivable pre (.ite guard thenBranch elseBranch) post
  | whileLoop {invariant : Assertion} {guard : BExp} {body : Cmd}
      (hbody : Derivable (fun state => invariant state ∧ guard.eval state = true)
        body invariant) :
      Derivable invariant (.while guard body)
        (fun state => invariant state ∧ guard.eval state = false)
  | consequence {pre pre' post post' : Assertion} {command : Cmd}
      (hpre : pre.Entails pre') (hderiv : Derivable pre' command post')
      (hpost : post'.Entails post) :
      Derivable pre command post
Uses 8 · Used by 11
Statement usesArithmetic expressions of IMP · Assertion · Entailment of assertions · Substitution in an assertion · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Commands of IMP · IMP program states
Used byRelative completeness of total-correctness Hoare logic · Total-correctness derivations give partial-correctness derivations · Partial-correctness Hoare logic matches the denotational semantics · Partial-correctness Hoare logic as an inference system · Derivability in the default inference system on Hoare triples is validity · The weakest liberal precondition gives a derivable triple · Soundness of Hoare logic for partial correctness · Precondition strengthening for partial correctness · Completeness of verification conditions for derivable triples · Completeness of verification conditions for valid triples · Soundness of verification conditions

TheoremSoundness of Hoare logic for partial correctness#✓fully proved

Every partial-correctness Hoare triple \(\{P\}\,c\,\{Q\}\) that is derivable in the partial-correctness proof system is valid: for all states \(s\) and \(s'\), if \(s\) satisfies \(P\) and \(c\) has a terminating big-step execution from \(s\) to \(s'\), then \(s'\) satisfies \(Q\).

theorem sound {pre post : Assertion} {command : Cmd}
    (h : Derivable pre command post) : Valid pre command post
Uses 13 · Used by 2
Statement usesAssertion · Commands of IMP · Derivability in Hoare logic for partial correctness · Validity of a Hoare triple
Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Entailment of assertions · Substitution in an assertion · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Big-step semantics of IMP · IMP program states · Invariant rule for while loops
Used byPartial-correctness Hoare logic as an inference system · Verification conditions yield valid Hoare triples

TheoremPrecondition strengthening for partial correctness#✓fully proved

Let \(P\), \(P'\) and \(Q\) be assertions and \(c\) a command. If \(P\) entails \(P'\) (every state satisfying \(P\) satisfies \(P'\)) and the partial-correctness triple \(\{P'\}\,c\,\{Q\}\) is derivable in the partial-correctness proof system, then so is \(\{P\}\,c\,\{Q\}\).

theorem strengthen {pre pre' post : Assertion} {command : Cmd}
    (hpre : pre.Entails pre') (h : Derivable pre' command post) :
    Derivable pre command post
Uses 5 · Used by 3
Statement usesAssertion · Entailment of assertions · Commands of IMP · Derivability in Hoare logic for partial correctness
Proof usesIMP program states
Used byRelative completeness of total-correctness Hoare logic · The weakest liberal precondition gives a derivable triple · Verification conditions yield valid Hoare triples

TheoremThe weakest liberal precondition gives a derivable triple#✓fully proved

For every command \(c\) and every assertion \(Q\), the triple whose precondition is the weakest liberal precondition of \(c\) with respect to \(Q\), whose command is \(c\) and whose postcondition is \(Q\) is derivable in partial-correctness Hoare logic.

theorem derivable_wlp : ∀ (command : Cmd) (post : Assertion),
    Derivable (wlp command post) command post
Uses 14 · Used by 1
Statement usesAssertion · Commands of IMP · Derivability in Hoare logic for partial correctness · Weakest liberal precondition
Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Entailment of assertions · Substitution in an assertion · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Big-step semantics of IMP · Precondition strengthening for partial correctness · IMP program states · Weakest liberal precondition unfolding of a while loop
Used byRelative completeness of total-correctness Hoare logic

TheoremRelative completeness of total-correctness Hoare logic#✓fully proved

For all assertions \(P\) and \(Q\) and every command \(c\), if the total-correctness triple with precondition \(P\), command \(c\) and postcondition \(Q\) is valid, then it is derivable in total-correctness Hoare logic.

theorem complete {pre post : Assertion} {command : Cmd}
    (h : Valid pre command post) : Derivable pre command post
Uses 10 · Used by 2
Statement usesAssertion · Commands of IMP · Derivability in Hoare logic for partial correctness · Validity of a Hoare triple
Proof usesEntailment of assertions · Big-step semantics of IMP · Precondition strengthening for partial correctness · IMP program states · The weakest liberal precondition gives a derivable triple · Weakest liberal precondition
Used byTotal-correctness derivations give partial-correctness derivations · Partial-correctness Hoare logic as an inference system

TheoremPartial-correctness Hoare logic as an inference system#✓fully proved

A Hoare triple, given by a precondition \(P\), a command \(c\) and a postcondition \(Q\), is derivable in the default inference system on Hoare triples, which is partial-correctness Hoare logic, if and only if it is valid for partial correctness.

theorem derivable_iff_valid {pre post : Assertion} {command : Cmd} :
    Derivable pre command post ↔ Valid pre command post
Uses 6 · Used by 3
Statement usesAssertion · Commands of IMP · Derivability in Hoare logic for partial correctness · Validity of a Hoare triple
Proof usesRelative completeness of total-correctness Hoare logic · Soundness of Hoare logic for partial correctness
Used byPartial-correctness Hoare logic matches the denotational semantics · Derivability in the default inference system on Hoare triples is validity · Completeness of verification conditions for valid triples

TheoremPartial-correctness Hoare logic matches the denotational semantics#✓fully proved

For all assertions \(P\) and \(Q\) and every command \(c\), the partial-correctness triple with precondition \(P\), command \(c\) and postcondition \(Q\) is derivable if and only if, for all states \(s\) and \(t\) such that \(P\) holds at \(s\) and the pair \((s, t)\) lies in the relational denotation of \(c\), \(Q\) holds at \(t\).

theorem derivable_iff_denote {pre post : Assertion} {command : Cmd} :
    Derivable pre command post ↔
      ∀ ⦃initial final⦄, pre initial → Denote command initial final → post final
Uses 9
Statement usesAssertion · Commands of IMP · Relational denotational semantics of IMP · Derivability in Hoare logic for partial correctness · IMP program states
Proof usesBig-step semantics of IMP · Agreement of the denotational and big-step semantics of IMP · Validity of a Hoare triple · Partial-correctness Hoare logic as an inference system

InductiveLoop runs with a given number of iterations#✓fully proved

Let \(b\) be a Boolean expression and \(c\) a command. For a natural number \(n\) and states \(s\), \(s'\), the loop \(\mathtt{while}\ b\ \mathtt{do}\ c\) runs from \(s\) to \(s'\) in \(n\) iterations when, started in \(s\), it exits in \(s'\) after exactly \(n\) executions of the body \(c\). This is the least relation such that the loop runs from \(s\) to \(s\) in \(0\) iterations whenever \(b\) evaluates to false in \(s\), and the loop runs from \(s\) to \(s'\) in \(n + 1\) iterations whenever \(b\) evaluates to true in \(s\), the body \(c\) has a terminating big-step execution from \(s\) to some state \(t\), and the loop runs from \(t\) to \(s'\) in \(n\) iterations.

inductive Iterates (guard : BExp) (body : Cmd) : Nat → State → State → Prop
  | exit {state : State} (hguard : guard.eval state = false) :
      Iterates guard body 0 state state
  | step {n : Nat} {initial middle final : State}
      (hguard : guard.eval initial = true) (hbody : BigStep body initial middle)
      (hrest : Iterates guard body n middle final) :
      Iterates guard body (n + 1) initial final
Uses 5 · Used by 7
Statement usesBoolean expressions of IMP · Evaluation of IMP Boolean expressions · Big-step semantics of IMP · Commands of IMP · IMP program states
Used byCounted loop runs are big-step executions · Uniqueness of the loop iteration count · Every terminating loop run has an iteration count · Loop iteration count · The iteration count of a terminating loop run · The iteration count of a nonterminating loop is zero · The weakest-precondition triple is derivable in total-correctness Hoare logic

TheoremCounted loop runs are big-step executions#✓fully proved

Let \(b\) be a boolean expression, \(c\) a command, \(n\) a natural number and \(s\), \(t\) states. If the loop \(\mathtt{while}\ b\ \mathtt{do}\ c\), started in \(s\), exits in \(t\) after exactly \(n\) executions of the body \(c\), then the loop \(\mathtt{while}\ b\ \mathtt{do}\ c\) runs from \(s\) to \(t\) in the big-step semantics.

theorem bigStep {n : Nat} {initial final : State}
    (h : Iterates guard body n initial final) :
    BigStep (.while guard body) initial final
Uses 6 · Used by 2
Statement usesBoolean expressions of IMP · Big-step semantics of IMP · Commands of IMP · Loop runs with a given number of iterations · IMP program states
Proof usesEvaluation of IMP Boolean expressions
Used byThe iteration count of a nonterminating loop is zero · The weakest-precondition triple is derivable in total-correctness Hoare logic

TheoremEvery terminating loop run has an iteration count#✓fully proved

Let \(b\) be a Boolean expression, \(c\) a command and \(s\), \(s'\) states. If the loop \(\mathtt{while}\ b\ \mathtt{do}\ c\) has a terminating big-step execution from \(s\) to \(s'\), then there is a natural number \(n\) such that the loop, started in \(s\), exits in \(s'\) after exactly \(n\) executions of the body \(c\).

theorem exists_of_bigStep {initial final : State}
    (h : BigStep (.while guard body) initial final) :
    ∃ n, Iterates guard body n initial final
Uses 8 · Used by 1
Statement usesBoolean expressions of IMP · Big-step semantics of IMP · Commands of IMP · Loop runs with a given number of iterations · IMP program states
Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Evaluation of IMP Boolean expressions
Used byThe weakest-precondition triple is derivable in total-correctness Hoare logic

TheoremUniqueness of the loop iteration count#✓fully proved

Let \(b\) be a boolean expression, \(c\) a command and \(s\) a state. If the loop \(\mathtt{while}\ b\ \mathtt{do}\ c\), started in \(s\), exits in a state \(t\) after exactly \(n\) executions of the body and also exits in a state \(t'\) after exactly \(m\) executions of the body, then \(n = m\).

theorem count_unique {n m : Nat} {initial first second : State}
    (hfirst : Iterates guard body n initial first)
    (hsecond : Iterates guard body m initial second) : n = m
Uses 7 · Used by 1
Statement usesBoolean expressions of IMP · Commands of IMP · Loop runs with a given number of iterations · IMP program states
Proof usesEvaluation of IMP Boolean expressions · Big-step semantics of IMP · Determinism of IMP big-step semantics
Used byThe iteration count of a terminating loop run

DefinitionLoop iteration count#✓fully proved

Let \(b\) be a Boolean expression, \(c\) a command and \(s\) a state. If there are a natural number \(n\) and a state \(s'\) such that the loop \(\mathtt{while}\ b\ \mathtt{do}\ c\), started in \(s\), exits in \(s'\) after exactly \(n\) executions of the body \(c\), then the iteration count of the loop from \(s\) is such an \(n\); otherwise it is \(0\).

Such an \(n\) is unique because IMP is deterministic, so the iteration count is the number of body executions the loop performs from \(s\) before exiting.

noncomputable def iterationCount (guard : BExp) (body : Cmd) (state : State) : Nat :=
  if h : ∃ n final, Iterates guard body n state final then Classical.choose h else 0
Uses 4 · Used by 3
Statement usesBoolean expressions of IMP · Commands of IMP · Loop runs with a given number of iterations · IMP program states
Used byThe iteration count of a terminating loop run · The iteration count of a nonterminating loop is zero · The weakest-precondition triple is derivable in total-correctness Hoare logic

TheoremThe iteration count of a terminating loop run#✓fully proved

Let \(b\) be a Boolean expression, \(c\) a command, \(n\) a natural number and \(s\), \(s'\) states. If the loop \(\mathtt{while}\ b\ \mathtt{do}\ c\), started in \(s\), exits in \(s'\) after exactly \(n\) executions of the body \(c\), then the iteration count of the loop from \(s\) is \(n\).

theorem Iterates.iterationCount_eq {guard : BExp} {body : Cmd} {n : Nat}
    {initial final : State} (h : Iterates guard body n initial final) :
    iterationCount guard body initial = n
Uses 6 · Used by 1
Statement usesBoolean expressions of IMP · Commands of IMP · Loop runs with a given number of iterations · IMP program states · Loop iteration count
Proof usesUniqueness of the loop iteration count
Used byThe weakest-precondition triple is derivable in total-correctness Hoare logic

TheoremThe iteration count of a nonterminating loop is zero#✓fully proved

Let \(b\) be a Boolean expression, \(c\) a command and \(s\) a state. If the loop \(\mathtt{while}\ b\ \mathtt{do}\ c\) has no terminating big-step execution from \(s\) to any state, then the iteration count of the loop from \(s\) is \(0\).

theorem iterationCount_eq_zero {guard : BExp} {body : Cmd} {state : State}
    (h : ∀ final, ¬ BigStep (.while guard body) state final) :
    iterationCount guard body state = 0
Uses 7
Statement usesBoolean expressions of IMP · Big-step semantics of IMP · Commands of IMP · IMP program states · Loop iteration count
Proof usesLoop runs with a given number of iterations · Counted loop runs are big-step executions

InductiveTotal-correctness Hoare logic#✓fully proved

Derivability of total-correctness Hoare triples \(\{P\}\,c\,\{Q\}\), for assertions \(P\), \(Q\) (predicates on states) and IMP commands \(c\), is the least relation closed under the following rules. In an assertion, \(b\) for a boolean expression means that \(b\) evaluates to true and \(\neg b\) that it evaluates to false. Skip: \(\{Q\}\,\mathtt{skip}\,\{Q\}\). Assignment: for a variable \(x\) and an arithmetic expression \(a\), \(\{Q[a/x]\}\,x := a\,\{Q\}\), where \(Q[a/x]\) holds in a state \(s\) iff \(Q\) holds in \(s\) updated at \(x\) to the value of \(a\) in \(s\). Sequencing: from \(\{P\}\,c_1\,\{R\}\) and \(\{R\}\,c_2\,\{Q\}\) derive \(\{P\}\,c_1; c_2\,\{Q\}\). Conditional: from \(\{P \wedge b\}\,c_1\,\{Q\}\) and \(\{P \wedge \neg b\}\,c_2\,\{Q\}\) derive \(\{P\}\,\mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2\,\{Q\}\). Loop (variant rule): for an assertion \(I\) and a map \(V\) from states to natural numbers, if for every natural number \(n\) the triple \(\{I \wedge b \wedge V = n\}\,c\,\{I \wedge V < n\}\) is derivable, derive \(\{I\}\,\mathtt{while}\ b\ \mathtt{do}\ c\,\{I \wedge \neg b\}\). Consequence: if \(P\) entails \(P'\), \(\{P'\}\,c\,\{Q'\}\) is derivable and \(Q'\) entails \(Q\), derive \(\{P\}\,c\,\{Q\}\), where entailment is pointwise implication.

Cslib.IMP.TDerivable · 24 lines 
inductive TDerivable : Assertion → Cmd → Assertion → Prop
  | skip (post : Assertion) : TDerivable post .skip post
  | assign (post : Assertion) (name : Nat) (value : AExp) :
      TDerivable (post.subst name value) (.assign name value) post
  | seq {pre middle post : Assertion} {first second : Cmd}
      (hfirst : TDerivable pre first middle) (hsecond : TDerivable middle second post) :
      TDerivable pre (.seq first second) post
  | ite {pre post : Assertion} {guard : BExp} {thenBranch elseBranch : Cmd}
      (hthen : TDerivable (fun state => pre state ∧ guard.eval state = true)
        thenBranch post)
      (helse : TDerivable (fun state => pre state ∧ guard.eval state = false)
        elseBranch post) :
      TDerivable pre (.ite guard thenBranch elseBranch) post
  | whileVariant {invariant : Assertion} {variant : State → Nat} {guard : BExp}
      {body : Cmd}
      (hbody : ∀ n : Nat, TDerivable
        (fun state => invariant state ∧ guard.eval state = true ∧ variant state = n)
        body (fun state => invariant state ∧ variant state < n)) :
      TDerivable invariant (.while guard body)
        (fun state => invariant state ∧ guard.eval state = false)
  | consequence {pre pre' post post' : Assertion} {command : Cmd}
      (hpre : pre.Entails pre') (hderiv : TDerivable pre' command post')
      (hpost : post'.Entails post) :
      TDerivable pre command post
Uses 8 · Used by 8
Statement usesArithmetic expressions of IMP · Assertion · Entailment of assertions · Substitution in an assertion · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Commands of IMP · IMP program states
Used byTotal-correctness Hoare logic is relatively complete · Total-correctness derivations give partial-correctness derivations · Total-correctness Hoare logic as an inference system · Soundness of total-correctness Hoare logic · Precondition strengthening for total correctness · Total-correctness Hoare logic is sound and complete for the denotational semantics · Soundness and relative completeness of total-correctness Hoare logic · The weakest-precondition triple is derivable in total-correctness Hoare logic

TheoremSoundness of total-correctness Hoare logic#✓fully proved

For all assertions \(P\) and \(Q\) and every command \(c\), if the triple \(\{P\}\,c\,\{Q\}\) is derivable in total-correctness Hoare logic, then it is valid for total correctness: every state satisfying \(P\) has a terminating big-step execution of \(c\) ending in a state that satisfies \(Q\).

theorem sound {pre post : Assertion} {command : Cmd}
    (h : TDerivable pre command post) : TValid pre command post
Uses 13 · Used by 2
Statement usesAssertion · Commands of IMP · Total-correctness Hoare logic · Validity of total-correctness Hoare triples
Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Entailment of assertions · Substitution in an assertion · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Big-step semantics of IMP · IMP program states · Variant rule for while loops
Used byTotal-correctness derivations give partial-correctness derivations · Soundness and relative completeness of total-correctness Hoare logic

TheoremPrecondition strengthening for total correctness#✓fully proved

Let \(P\), \(P'\) and \(Q\) be assertions and \(c\) a command. If \(P\) entails \(P'\) (every state satisfying \(P\) satisfies \(P'\)) and the triple \(\{P'\}\,c\,\{Q\}\) is derivable in total-correctness Hoare logic, then so is \(\{P\}\,c\,\{Q\}\).

theorem strengthen {pre pre' post : Assertion} {command : Cmd}
    (hpre : pre.Entails pre') (h : TDerivable pre' command post) :
    TDerivable pre command post
Uses 5 · Used by 2
Statement usesAssertion · Entailment of assertions · Commands of IMP · Total-correctness Hoare logic
Proof usesIMP program states
Used byTotal-correctness Hoare logic is relatively complete · The weakest-precondition triple is derivable in total-correctness Hoare logic

TheoremThe weakest-precondition triple is derivable in total-correctness Hoare logic#✓fully proved

For every IMP command \(c\) and every assertion \(Q\) (a predicate on states), the triple \(\{\mathrm{wp}(c, Q)\}\,c\,\{Q\}\) is derivable in the total-correctness Hoare logic. Here \(\mathrm{wp}(c, Q)\) is the semantic weakest precondition: it holds in a state \(s\) exactly when there is a terminating execution of \(c\) from \(s\) ending in a state satisfying \(Q\).

theorem tderivable_wp : ∀ (command : Cmd) (post : Assertion),
    TDerivable (wp command post) command post
Uses 18 · Used by 1
Statement usesAssertion · Commands of IMP · Total-correctness Hoare logic · Weakest precondition for total correctness
Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Entailment of assertions · Substitution in an assertion · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Big-step semantics of IMP · Loop runs with a given number of iterations · Counted loop runs are big-step executions · Every terminating loop run has an iteration count · The iteration count of a terminating loop run · IMP program states · Precondition strengthening for total correctness · Loop iteration count
Used byTotal-correctness Hoare logic is relatively complete

TheoremTotal-correctness Hoare logic is relatively complete#✓fully proved

For all assertions \(P\) and \(Q\) and every command \(c\), if the total-correctness Hoare triple \(\{P\}\,c\,\{Q\}\) is valid, then it is derivable in total-correctness Hoare logic.

theorem complete {pre post : Assertion} {command : Cmd}
    (h : TValid pre command post) : TDerivable pre command post
Uses 10 · Used by 1
Statement usesAssertion · Commands of IMP · Total-correctness Hoare logic · Validity of total-correctness Hoare triples
Proof usesEntailment of assertions · Big-step semantics of IMP · IMP program states · Precondition strengthening for total correctness · The weakest-precondition triple is derivable in total-correctness Hoare logic · Weakest precondition for total correctness
Used bySoundness and relative completeness of total-correctness Hoare logic

TheoremTotal-correctness derivations give partial-correctness derivations#✓fully proved

For all assertions \(P\) and \(Q\) and every command \(c\), if the triple with precondition \(P\), command \(c\) and postcondition \(Q\) is derivable in total-correctness Hoare logic, then it is derivable in partial-correctness Hoare logic.

theorem derivable {pre post : Assertion} {command : Cmd}
    (h : TDerivable pre command post) : Derivable pre command post
Uses 7
Statement usesAssertion · Commands of IMP · Derivability in Hoare logic for partial correctness · Total-correctness Hoare logic
Proof usesRelative completeness of total-correctness Hoare logic · Soundness of total-correctness Hoare logic · Total correctness implies partial correctness

TheoremSoundness and relative completeness of total-correctness Hoare logic#✓fully proved

For all assertions \(P\), \(Q\) (predicates on states) and every IMP command \(c\), the triple \(\{P\}\,c\,\{Q\}\) is derivable in the total-correctness Hoare logic if and only if it is totally valid.

theorem tderivable_iff_tvalid {pre post : Assertion} {command : Cmd} :
    TDerivable pre command post ↔ TValid pre command post
Uses 6 · Used by 2
Statement usesAssertion · Commands of IMP · Total-correctness Hoare logic · Validity of total-correctness Hoare triples
Proof usesTotal-correctness Hoare logic is relatively complete · Soundness of total-correctness Hoare logic
Used byTotal-correctness Hoare logic as an inference system · Total-correctness Hoare logic is sound and complete for the denotational semantics

TheoremTotal-correctness Hoare logic is sound and complete for the denotational semantics#✓fully proved

For all assertions \(P\), \(Q\) (predicates on states) and every IMP command \(c\), the triple \(\{P\}\,c\,\{Q\}\) is derivable in the total-correctness Hoare logic if and only if for every state \(s\) satisfying \(P\) there is a state \(s'\) such that \((s, s')\) lies in the relational denotation of \(c\) and \(s'\) satisfies \(Q\).

theorem tderivable_iff_denote {pre post : Assertion} {command : Cmd} :
    TDerivable pre command post ↔
      ∀ ⦃initial⦄, pre initial → ∃ final, Denote command initial final ∧ post final
Uses 9
Statement usesAssertion · Commands of IMP · Relational denotational semantics of IMP · IMP program states · Total-correctness Hoare logic
Proof usesBig-step semantics of IMP · Agreement of the denotational and big-step semantics of IMP · Validity of total-correctness Hoare triples · Soundness and relative completeness of total-correctness Hoare logic

StructureHoare triples#✓fully proved

A Hoare triple \(\{P\}\,c\,\{Q\}\) consists of a precondition \(P\) and a postcondition \(Q\), both assertions (predicates on states), and an IMP command \(c\). It is the judgement form of both the partial-correctness and the total-correctness Hoare logic.

structure Triple where
  /-- The precondition. -/
  pre : Assertion
  /-- The command. -/
  command : Cmd
  /-- The postcondition. -/
  post : Assertion
Uses 2 · Used by 2
Statement usesAssertion · Commands of IMP
Used byDerivability in the default inference system on Hoare triples is validity · Total-correctness Hoare logic as an inference system

InductiveTotal-correctness tag for Hoare triples#✓fully proved

An empty type used only as a label: derivability of Hoare triples in the total-correctness Hoare logic is registered as an inference system under this tag, while partial-correctness derivability is the default inference system on Hoare triples.

inductive TotalCorrectness : Type
Used by 1
Used byTotal-correctness Hoare logic as an inference system

TheoremDerivability in the default inference system on Hoare triples is validity#✓fully proved

For every Hoare triple \(\{P\}\,c\,\{Q\}\), the triple is derivable in the default inference system on Hoare triples, which is partial-correctness Hoare logic, if and only if it is valid for partial correctness.

theorem derivable_iff_valid (t : Triple) :
    Cslib.Logic.InferenceSystem.Derivable t ↔ Valid t.pre t.command t.post
Uses 6
Statement usesAssertion · Commands of IMP · Derivability in Hoare logic for partial correctness · Hoare triples · Validity of a Hoare triple
Proof usesPartial-correctness Hoare logic as an inference system

TheoremTotal-correctness Hoare logic as an inference system#✓fully proved

A Hoare triple, given by a precondition \(P\), a command \(c\) and a postcondition \(Q\), is derivable in the inference system on Hoare triples tagged total correctness, which is total-correctness Hoare logic, if and only if it is valid for total correctness.

theorem derivableIn_totalCorrectness_iff_tvalid (t : Triple) :
    Cslib.Logic.InferenceSystem.DerivableIn TotalCorrectness t ↔
      TValid t.pre t.command t.post
Uses 7
Statement usesAssertion · Commands of IMP · Total-correctness Hoare logic · Validity of total-correctness Hoare triples · Total-correctness tag for Hoare triples · Hoare triples
Proof usesSoundness and relative completeness of total-correctness Hoare logic
41 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.