Verification-condition generation

9 fully proved

IMP

InductiveAnnotated commands#✓fully proved

An annotated command is built like an IMP command, from skip, assignments \(x := a\) of an arithmetic expression \(a\) to a variable \(x\) (a natural number), sequential composition \(C_1;\,C_2\) and conditionals \(\mathrm{if}\ b\ \mathrm{then}\ C_1\ \mathrm{else}\ C_2\) on a boolean expression \(b\), except that every while loop \(\{I\}\ \mathrm{while}\ b\ \mathrm{do}\ C\) also carries an assertion \(I\), its invariant.

inductive ACmd where
  | skip
  | assign (name : Nat) (value : AExp)
  | seq (first second : ACmd)
  | ite (guard : BExp) (thenBranch elseBranch : ACmd)
  | while (invariant : Assertion) (guard : BExp) (body : ACmd)

Uses 3 · Used by 8

Statement usesArithmetic expressions of IMP · Assertion · Boolean expressions of IMP

Used byPrecondition 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

Annotated commands and verification conditions

DefinitionErasing annotations#✓fully proved

The IMP command \(\mathrm{strip}(C)\) underlying an annotated command \(C\) is obtained by deleting the invariant of every while loop: skip, assignments, sequential composition and conditionals are kept with their parts stripped, and \(\{I\}\ \mathrm{while}\ b\ \mathrm{do}\ C'\) becomes \(\mathrm{while}\ b\ \mathrm{do}\ \mathrm{strip}(C')\).

def strip : ACmd → Cmd
  | .skip => .skip
  | .assign name value => .assign name value
  | .seq first second => .seq first.strip second.strip
  | .ite guard thenBranch elseBranch => .ite guard thenBranch.strip elseBranch.strip
  | .while _ guard body => .while guard body.strip

Uses 5 · Used by 4

Statement usesAnnotated commands · Arithmetic expressions of IMP · Assertion · Boolean expressions of IMP · Commands of IMP

Used byCompleteness of verification conditions for derivable triples · Completeness of verification conditions for valid triples · Soundness of verification conditions · Verification conditions yield valid Hoare triples

DefinitionPrecondition of an annotated command#✓fully proved

For an annotated command \(C\) and an assertion \(Q\) (the postcondition), the precondition \(\mathrm{pre}(C, Q)\) is the assertion computed backwards as follows: \(\mathrm{pre}(\mathrm{skip}, Q) = Q\); \(\mathrm{pre}(x := a, Q)\) holds in a state \(s\) iff \(Q\) holds in the state obtained from \(s\) by giving \(x\) the value of \(a\) in \(s\); \(\mathrm{pre}(C_1;\,C_2, Q) = \mathrm{pre}(C_1, \mathrm{pre}(C_2, Q))\); the precondition of \(\mathrm{if}\ b\ \mathrm{then}\ C_1\ \mathrm{else}\ C_2\) for \(Q\) holds in a state \(s\) iff \(\mathrm{pre}(C_1, Q)\) holds in \(s\) when \(b\) is true in \(s\), and \(\mathrm{pre}(C_2, Q)\) holds in \(s\) when \(b\) is false in \(s\); and the precondition of a loop \(\{I\}\ \mathrm{while}\ b\ \mathrm{do}\ C\) is its invariant \(I\), whatever \(Q\) is.

def pre : ACmd → Assertion → Assertion
  | .skip, post => post
  | .assign name value, post => post.subst name value
  | .seq first second, post => first.pre (second.pre post)
  | .ite guard thenBranch elseBranch, post => fun state =>
      if guard.eval state = true then thenBranch.pre post state
      else elseBranch.pre post state
  | .while invariant _ _, _ => invariant

Uses 7 · Used by 6

Statement usesAnnotated commands · Arithmetic expressions of IMP · Assertion · Substitution in an assertion · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · IMP program states

Used byWeakening the postcondition of an annotated command · 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

DefinitionVerification condition of an annotated command#✓fully proved

For an annotated command \(C\) and an assertion \(Q\) (the postcondition), the verification condition \(\mathrm{vc}(C, Q)\) is the proposition defined as follows, where \(\mathrm{pre}\) is the precondition of an annotated command: \(\mathrm{vc}(\mathrm{skip}, Q)\) and \(\mathrm{vc}(x := a, Q)\) are true; \(\mathrm{vc}(C_1;\,C_2, Q)\) holds iff \(\mathrm{vc}(C_1, \mathrm{pre}(C_2, Q))\) and \(\mathrm{vc}(C_2, Q)\) hold; the verification condition of \(\mathrm{if}\ b\ \mathrm{then}\ C_1\ \mathrm{else}\ C_2\) for \(Q\) holds iff \(\mathrm{vc}(C_1, Q)\) and \(\mathrm{vc}(C_2, Q)\) hold; and for a loop \(\{I\}\ \mathrm{while}\ b\ \mathrm{do}\ C'\), the verification condition for \(Q\) holds iff every state satisfying \(I\) in which \(b\) is true satisfies \(\mathrm{pre}(C', I)\), every state satisfying \(I\) in which \(b\) is false satisfies \(Q\), and \(\mathrm{vc}(C', I)\) holds.

def vc : ACmd → Assertion → Prop
  | .skip, _ => True
  | .assign _ _, _ => True
  | .seq first second, post => first.vc (second.pre post) ∧ second.vc post
  | .ite _ thenBranch elseBranch, post => thenBranch.vc post ∧ elseBranch.vc post
  | .while invariant guard body, post =>
      (∀ state, invariant state → guard.eval state = true → body.pre invariant state) ∧
      (∀ state, invariant state → guard.eval state = false → post state) ∧
      body.vc invariant

Uses 7 · Used by 5

Statement usesAnnotated commands · Precondition of an annotated command · Arithmetic expressions of IMP · Assertion · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · IMP program states

Used byWeakening 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

TheoremSoundness of verification conditions#✓fully proved

For an annotated command \(C\) and an assertion \(Q\), write \(\mathrm{pre}(C, Q)\) and \(\mathrm{vc}(C, Q)\) for the precondition and the verification condition of \(C\) for the postcondition \(Q\), and \(\mathrm{strip}(C)\) for the IMP command obtained from \(C\) by erasing its loop invariants. For every such \(C\) and \(Q\), if \(\mathrm{vc}(C, Q)\) holds, then the Hoare triple \(\{\mathrm{pre}(C, Q)\}\ \mathrm{strip}(C)\ \{Q\}\) is derivable in the partial-correctness Hoare logic.

theorem vc_sound : ∀ (C : ACmd) (post : Assertion), C.vc post →
    Derivable (C.pre post) C.strip post

Uses 13 · Used by 1

Statement usesAnnotated commands · Precondition of an annotated command · Erasing annotations · Verification condition of an annotated command · Assertion · Derivability in Hoare logic for partial correctness

Proof usesArithmetic expressions of IMP · Entailment of assertions · Substitution in an assertion · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Commands of IMP · IMP program states

Used byVerification conditions yield valid Hoare triples

TheoremVerification conditions yield valid Hoare triples#✓fully proved

Let \(C\) be an annotated command, let \(\mathrm{strip}(C)\) be the IMP command obtained from \(C\) by erasing its loop invariants, and let \(P\), \(Q\) be assertions. If the verification condition \(\mathrm{vc}(C, Q)\) holds and \(P\) entails the precondition \(\mathrm{pre}(C, Q)\), then the partial-correctness Hoare triple \(\{P\}\ \mathrm{strip}(C)\ \{Q\}\) is valid.

theorem vc_valid {C : ACmd} {pre' post : Assertion} (hvc : C.vc post)
    (hpre : pre'.Entails (C.pre post)) : Valid pre' C.strip post

Uses 10

Statement usesAnnotated commands · Precondition of an annotated command · Erasing annotations · Verification condition of an annotated command · Assertion · Entailment of assertions · Validity of a Hoare triple

Proof usesSoundness of verification conditions · Soundness of Hoare logic for partial correctness · Precondition strengthening for partial correctness

TheoremWeakening the postcondition of an annotated command#✓fully proved

Let \(C\) be an annotated command and \(Q\), \(Q'\) assertions such that \(Q\) entails \(Q'\), and write \(\mathrm{pre}(C, Q)\) and \(\mathrm{vc}(C, Q)\) for the precondition and the verification condition of \(C\) for the postcondition \(Q\). If \(\mathrm{vc}(C, Q)\) holds, then \(\mathrm{pre}(C, Q)\) entails \(\mathrm{pre}(C, Q')\) and \(\mathrm{vc}(C, Q')\) holds.

theorem pre_entails_vc : ∀ (C : ACmd) {post post' : Assertion}, post.Entails post' →
    C.vc post → (C.pre post).Entails (C.pre post') ∧ C.vc post'

Uses 10 · Used by 1

Statement usesAnnotated commands · Precondition of an annotated command · Verification condition of an annotated command · Assertion · Entailment of assertions

Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · IMP program states

Used byCompleteness of verification conditions for derivable triples

TheoremCompleteness of verification conditions for derivable triples#✓fully proved

Let \(c\) be an IMP command and \(P\), \(Q\) assertions such that the Hoare triple \(\{P\}\ c\ \{Q\}\) is derivable in the partial-correctness Hoare logic. Then there is an annotated command \(C\) such that erasing its loop invariants gives \(c\), that is \(\mathrm{strip}(C) = c\), the verification condition \(\mathrm{vc}(C, Q)\) holds, and \(P\) entails the precondition \(\mathrm{pre}(C, Q)\).

theorem vc_complete {pre' post : Assertion} {command : Cmd}
    (h : Derivable pre' command post) :
    ∃ C : ACmd, C.strip = command ∧ C.vc post ∧ pre'.Entails (C.pre post)

Uses 14 · Used by 1

Statement usesAnnotated commands · Precondition of an annotated command · Erasing annotations · Verification condition of an annotated command · Assertion · Entailment of assertions · Commands of IMP · Derivability in Hoare logic for partial correctness

Proof usesWeakening the postcondition of an annotated command · Arithmetic expressions of IMP · Substitution in an assertion · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · IMP program states

Used byCompleteness of verification conditions for valid triples

TheoremCompleteness of verification conditions for valid triples#✓fully proved

Let \(c\) be an IMP command and \(P\), \(Q\) assertions such that the partial-correctness Hoare triple \(\{P\}\ c\ \{Q\}\) is valid. Then there is an annotated command \(C\) such that erasing its loop invariants gives \(c\), that is \(\mathrm{strip}(C) = c\), the verification condition \(\mathrm{vc}(C, Q)\) holds, and \(P\) entails the precondition \(\mathrm{pre}(C, Q)\).

The proof goes through relative completeness of the Hoare logic.

theorem vc_complete_of_valid {pre' post : Assertion} {command : Cmd}
    (h : Valid pre' command post) :
    ∃ C : ACmd, C.strip = command ∧ C.vc post ∧ pre'.Entails (C.pre post)

Uses 11

Statement usesAnnotated commands · Precondition of an annotated command · Erasing annotations · Verification condition of an annotated command · Assertion · Entailment of assertions · Commands of IMP · Validity of a Hoare triple

Proof usesCompleteness of verification conditions for derivable triples · Derivability in Hoare logic for partial correctness · Partial-correctness Hoare logic as an inference system

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.