Operational semantics of IMP

AbbreviationIMP program states#✓fully proved

A state of an IMP program is a function \(\sigma : \mathbb{N} \to \mathbb{N}\) assigning a natural-number value \(\sigma(i)\) to each variable, where variables are identified by natural numbers \(i\).

abbrev State := Nat → Nat

Used by 107

Used byAssertion · Counted loop runs are big-step executions · Relative completeness of total-correctness Hoare logic · Total-correctness Hoare logic is relatively complete · Uniqueness of the loop iteration count · Derivability in Hoare logic for partial correctness · Partial-correctness Hoare logic matches the denotational semantics · The weakest liberal precondition gives a derivable triple · Entailment of assertions · Every terminating loop run has an iteration count · Loop invariants entail the weakest liberal precondition of the loop · Loop runs with a given number of iterations · Loop iteration count · The iteration count of a terminating loop run · The iteration count of a nonterminating loop is zero · 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 · The weakest-precondition triple is derivable in total-correctness Hoare logic · Total correctness gives a terminating small-step run · 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 · Assignment rule with a store-irrelevant heap assertion · Empty-heap assertion · Entailment of heap assertions · Existential rule for separation-logic triples · Frame rule · Store-irrelevant frames satisfy the frame-rule side condition · Conjunction of heap assertions · Heap assertion · Existential heap assertion · Hoare validity embeds into separation validity · Framed embedding of Hoare validity · Points-to assertion · Pure assertion · Local rule for a heap read · Separation-logic triple validity · Separating conjunction · Pulling a store fact out of a separating conjunction · Rearranging a separating conjunction · Store-irrelevant heap assertions · Separation-logic while rule · Precondition of an annotated command · Weakening the postcondition of an annotated command · Verification condition of an annotated command · Completeness of verification conditions for derivable triples · Soundness of verification conditions · Compiled arithmetic code pushes the value of the expression · Compiled Boolean code pushes the truth value of the expression · Correctness of compilation to the stack machine · Compiled command code simulates big-step execution · Stack machine configurations · Determinism of the stack machine · No step past the end of the program · Step relation of the stack machine · Denotational executions are big-step executions · Relational denotational semantics of IMP · Big-step executions are denotational executions · The denotational semantics of IMP is deterministic · Agreement of the denotational and big-step semantics of IMP · The while denotation is a fixed point · One-step unfolding functional of a while loop · Monotonicity of the while-loop unfolding functional · Unfolding equation for the while denotation · Park induction for while loops · The while-loop functional as a monotone map · Frame decomposition of heap executions · Frame decomposition of a single heap step · Adding a frame heap preserves the ability to step · Heap configurations · Small-step semantics of heap commands · Steps do not enlarge the modified variables · Executions of embedded commands are plain executions · Safe heap configurations · Embedded plain commands are safe · A heap step only changes assignable variables · Heap executions only change assignable variables · Embedding preserves termination · Heap steps of embedded commands are plain steps · Plain executions lift to the heap language · Big-step semantics of IMP · IMP configuration · Determinism of IMP big-step semantics · Small-step termination is deterministic · Determinism of IMP small-step semantics · Evaluation of IMP arithmetic expressions · Evaluation of IMP Boolean expressions · Hoare validity via small-step termination · Big-step executions terminate in small steps · Prepending one small step to a big-step execution · Prepending finitely many small steps to a big-step execution · Small-step termination implies big-step evaluation · IMP small-step relation · Termination of an IMP command · Equivalence of small-step and big-step semantics

InductiveArithmetic expressions of IMP#✓fully proved

The arithmetic expressions of IMP are built inductively from the constants \(n\), one for each natural number \(n\), and the variables \(x_i\), one for each natural number \(i\): if \(a_1\) and \(a_2\) are arithmetic expressions, then so are \(a_1 + a_2\), \(a_1 - a_2\) and \(a_1 \cdot a_2\).

inductive AExp where
  | const (value : Nat)
  | var (name : Nat)
  | add (left right : AExp)
  | sub (left right : AExp)
  | mul (left right : AExp)
  deriving DecidableEq, Repr

Used by 56

Used byDerivability in Hoare logic for partial correctness · The weakest liberal precondition gives a derivable triple · Every terminating loop run has an iteration count · Soundness of Hoare logic for partial correctness · Soundness of total-correctness Hoare logic · Substitution in an assertion · Total-correctness Hoare logic · The weakest-precondition triple is derivable in total-correctness Hoare logic · Weakest-precondition unfolding of a while loop · Invariant rule for while loops · Weakest liberal precondition unfolding of a while loop · Assignment rule with a store-irrelevant heap assertion · Hoare validity embeds into separation validity · Local rule for a heap read · Separation-logic while rule · 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 · Soundness of verification conditions · Instruction count of an arithmetic expression · Instruction count of a Boolean expression · Instruction count of a command · Compilation of commands · Compilation of arithmetic expressions · Compiled arithmetic code pushes the value of the expression · Compilation of Boolean expressions · Compiled Boolean code pushes the truth value of the expression · Compiled command code simulates big-step execution · Denotational executions are big-step executions · Relational denotational semantics of IMP · Big-step executions are denotational executions · Frame decomposition of heap executions · Frame decomposition of a single heap step · Adding a frame heap preserves the ability to step · Heap commands · Small-step semantics of heap commands · Modified variables of a heap command · Steps do not enlarge the modified variables · Embedded plain commands are safe · A heap step only changes assignable variables · Embedding preserves termination · Embedding of IMP into the heap language · Heap steps of embedded commands are plain steps · Boolean expressions of IMP · Big-step semantics of IMP · Commands of IMP · Determinism of IMP big-step semantics · Determinism of IMP small-step semantics · Evaluation of IMP arithmetic expressions · Evaluation of IMP Boolean expressions · Big-step executions terminate in small steps · Prepending one small step to a big-step execution · IMP small-step relation

InductiveBoolean expressions of IMP#✓fully proved

The Boolean expressions of IMP are built inductively from the constants true and false and the comparisons \(a_1 = a_2\) and \(a_1 \le a_2\) of arithmetic expressions \(a_1, a_2\): if \(b\), \(b_1\) and \(b_2\) are Boolean expressions, then so are the negation \(\neg b\) and the conjunction \(b_1 \wedge b_2\).

inductive BExp where
  | truth (value : Bool)
  | eq (left right : AExp)
  | le (left right : AExp)
  | not (body : BExp)
  | and (left right : BExp)
  deriving DecidableEq, Repr

Uses 1 · Used by 64

Statement usesArithmetic expressions of IMP

Used byCounted loop runs are big-step executions · Uniqueness of the loop iteration count · Derivability in Hoare logic for partial correctness · The weakest liberal precondition gives a derivable triple · Every terminating loop run has an iteration count · Loop invariants entail the weakest liberal precondition of the loop · Loop runs with a given number of iterations · Loop iteration count · The iteration count of a terminating loop run · The iteration count of a nonterminating loop is zero · 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 · 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 · Assignment rule with a store-irrelevant heap assertion · Hoare validity embeds into separation validity · Local rule for a heap read · Separation-logic while rule · 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 · Soundness of verification conditions · Instruction count of a Boolean expression · Instruction count of a command · Compilation of commands · Compilation of Boolean expressions · Compiled Boolean code pushes the truth value of the expression · Compiled command code simulates big-step execution · Denotational executions are big-step executions · Relational denotational semantics of IMP · Big-step executions are denotational executions · The while denotation is a fixed point · One-step unfolding functional of a while loop · Monotonicity of the while-loop unfolding functional · Unfolding equation for the while denotation · Park induction for while loops · The while-loop functional as a monotone map · Frame decomposition of heap executions · Frame decomposition of a single heap step · Adding a frame heap preserves the ability to step · Heap commands · Small-step semantics of heap commands · Modified variables of a heap command · Steps do not enlarge the modified variables · Embedded plain commands are safe · A heap step only changes assignable variables · Embedding preserves termination · Embedding of IMP into the heap language · Heap steps of embedded commands are plain steps · Big-step semantics of IMP · Commands of IMP · Determinism of IMP big-step semantics · Determinism of IMP small-step semantics · Evaluation of IMP Boolean expressions · Big-step executions terminate in small steps · Prepending one small step to a big-step execution · IMP small-step relation

InductiveCommands of IMP#✓fully proved

The commands of the while-language IMP are built inductively from skip and the assignments \(x_i := a\) of an arithmetic expression \(a\) to the variable \(x_i\) with index \(i \in \mathbb{N}\): if \(c\), \(c_1\) and \(c_2\) are commands and \(b\) is a Boolean expression, then so are the sequential composition \(c_1 ; c_2\), the conditional if \(b\) then \(c_1\) else \(c_2\), and the loop while \(b\) do \(c\).

inductive Cmd where
  | skip
  | assign (name : Nat) (value : AExp)
  | seq (first second : Cmd)
  | ite (guard : BExp) (thenBranch elseBranch : Cmd)
  | while (guard : BExp) (body : Cmd)
  deriving DecidableEq, Repr

Uses 2 · Used by 74

Statement usesArithmetic expressions of IMP · Boolean expressions of IMP

Used byCounted loop runs are big-step executions · Relative completeness of total-correctness Hoare logic · Total-correctness Hoare logic is relatively complete · Uniqueness of the loop iteration count · 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 · Every terminating loop run has an iteration count · Loop invariants entail the weakest liberal precondition of the loop · Loop runs with a given number of iterations · Loop iteration count · The iteration count of a terminating loop run · The iteration count of a nonterminating loop is zero · 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 · 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 · Erasing annotations · Completeness of verification conditions for derivable triples · Completeness of verification conditions for valid triples · Soundness of verification conditions · Instruction count of a command · Compilation of commands · Correctness of compilation to the stack machine · Compiled command code simulates big-step execution · Denotational executions are big-step executions · Relational denotational semantics of IMP · Big-step executions are denotational executions · The denotational semantics of IMP is deterministic · Agreement of the denotational and big-step semantics of IMP · The while denotation is a fixed point · Unfolding equation for the while denotation · Park induction for while loops · Executions of embedded commands are plain executions · Embedded plain commands are safe · Embedding preserves termination · Embedding of IMP into the heap language · Heap steps of embedded commands are plain steps · Plain executions lift to the heap language · Big-step semantics of IMP · IMP configuration · Determinism of IMP big-step semantics · Small-step termination is deterministic · Determinism of IMP small-step semantics · Hoare validity via small-step termination · Big-step executions terminate in small steps · Prepending one small step to a big-step execution · Prepending finitely many small steps to a big-step execution · Small-step termination implies big-step evaluation · IMP small-step relation · Termination of an IMP command · Equivalence of small-step and big-step semantics

DefinitionEvaluation of IMP arithmetic expressions#✓fully proved

The value of an arithmetic expression in a state \(\sigma : \mathbb{N} \to \mathbb{N}\) is the natural number defined by recursion on the expression: a constant \(n\) has value \(n\), the variable \(x_i\) with index \(i\) has value \(\sigma(i)\), and for arithmetic expressions \(a_1\) and \(a_2\), the expressions \(a_1 + a_2\), \(a_1 - a_2\) and \(a_1 \cdot a_2\) have as value the sum, the truncated difference and the product of the values of \(a_1\) and \(a_2\). The truncated difference of natural numbers \(m\) and \(n\) is \(\max(m - n, 0)\).

def eval : AExp → State → Nat
  | .const value, _ => value
  | .var name, state => state name
  | .add left right, state => left.eval state + right.eval state
  | .sub left right, state => left.eval state - right.eval state
  | .mul left right, state => left.eval state * right.eval state

Uses 2 · Used by 34

Statement usesArithmetic expressions of IMP · IMP program states

Used byThe weakest liberal precondition gives a derivable triple · Every terminating loop run has an iteration count · Soundness of Hoare logic for partial correctness · Soundness of total-correctness Hoare logic · Substitution in an assertion · The weakest-precondition triple is derivable in total-correctness Hoare logic · Weakest-precondition unfolding of a while loop · Invariant rule for while loops · Weakest liberal precondition unfolding of a while loop · Assignment rule with a store-irrelevant heap assertion · Local rule for a heap read · Separation-logic while rule · Weakening the postcondition of an annotated command · Compiled arithmetic code pushes the value of the expression · Compiled Boolean code pushes the truth value of the expression · Compiled command code simulates big-step execution · Denotational executions are big-step executions · Relational denotational semantics of IMP · Big-step executions are denotational executions · Frame decomposition of heap executions · Frame decomposition of a single heap step · Adding a frame heap preserves the ability to step · Small-step semantics of heap commands · Steps do not enlarge the modified variables · Embedded plain commands are safe · A heap step only changes assignable variables · Heap steps of embedded commands are plain steps · Big-step semantics of IMP · Determinism of IMP big-step semantics · Determinism of IMP small-step semantics · Evaluation of IMP Boolean expressions · Big-step executions terminate in small steps · Prepending one small step to a big-step execution · IMP small-step relation

DefinitionEvaluation of IMP Boolean expressions#✓fully proved

The truth value of a Boolean expression in a state \(\sigma : \mathbb{N} \to \mathbb{N}\) is defined by recursion on the expression: the constants true and false have values true and false; for arithmetic expressions \(a_1\) and \(a_2\), the comparison \(a_1 = a_2\) is true exactly when the values of \(a_1\) and \(a_2\) in \(\sigma\) are equal, and \(a_1 \le a_2\) is true exactly when the value of \(a_1\) is at most the value of \(a_2\); for Boolean expressions \(b\), \(b_1\) and \(b_2\), the negation \(\neg b\) is true exactly when \(b\) is false, and the conjunction \(b_1 \wedge b_2\) is true exactly when both \(b_1\) and \(b_2\) are true.

def eval : BExp → State → Bool
  | .truth value, _ => value
  | .eq left right, state => decide (left.eval state = right.eval state)
  | .le left right, state => decide (left.eval state ≤ right.eval state)
  | .not body, state => !body.eval state
  | .and left right, state => left.eval state && right.eval state

Uses 4 · Used by 45

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

Used byCounted loop runs are big-step executions · Uniqueness of the loop iteration count · Derivability in Hoare logic for partial correctness · The weakest liberal precondition gives a derivable triple · Every terminating loop run has an iteration count · Loop invariants entail the weakest liberal precondition of the loop · Loop runs with a given number of iterations · 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 · 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 · Assignment rule with a store-irrelevant heap assertion · Local rule for a heap read · Separation-logic while rule · Precondition of an annotated command · Weakening the postcondition of an annotated command · Verification condition of an annotated command · Completeness of verification conditions for derivable triples · Soundness of verification conditions · Compiled Boolean code pushes the truth value of the expression · Compiled command code simulates big-step execution · Denotational executions are big-step executions · Relational denotational semantics of IMP · Big-step executions are denotational executions · One-step unfolding functional of a while loop · Monotonicity of the while-loop unfolding functional · Unfolding equation for the while denotation · Frame decomposition of heap executions · Frame decomposition of a single heap step · Adding a frame heap preserves the ability to step · Small-step semantics of heap commands · Steps do not enlarge the modified variables · Embedded plain commands are safe · A heap step only changes assignable variables · Heap steps of embedded commands are plain steps · Big-step semantics of IMP · Determinism of IMP big-step semantics · Determinism of IMP small-step semantics · Big-step executions terminate in small steps · Prepending one small step to a big-step execution · IMP small-step relation

InductiveBig-step semantics of IMP#✓fully proved

The big-step relation says when running a command \(c\) from a state \(s\) terminates in a state \(t\); we then say that \(c\) takes \(s\) to \(t\). It is the least relation satisfying the following rules. The command \(\mathtt{skip}\) takes \(s\) to \(s\). The assignment \(x := a\) takes \(s\) to the state \(s[x \mapsto a(s)]\), which agrees with \(s\) except that \(x\) has the value \(a(s)\) of the arithmetic expression \(a\) in \(s\). If \(c_1\) takes \(s\) to \(u\) and \(c_2\) takes \(u\) to \(t\), then the sequence \(c_1 ; c_2\) takes \(s\) to \(t\). If the Boolean expression \(b\) is true in \(s\) and \(c_1\) takes \(s\) to \(t\), then \(\mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2\) takes \(s\) to \(t\); if \(b\) is false in \(s\) and \(c_2\) takes \(s\) to \(t\), then it also takes \(s\) to \(t\). If \(b\) is false in \(s\), then the loop \(\mathtt{while}\ b\ \mathtt{do}\ c\) takes \(s\) to \(s\); if \(b\) is true in \(s\), \(c\) takes \(s\) to \(u\) and the loop takes \(u\) to \(t\), then the loop takes \(s\) to \(t\).

Cslib.IMP.BigStep · 24 lines

inductive BigStep : Cmd → State → State → Prop
  | skip (state) : BigStep .skip state state
  | assign (state) (name) (value) :
      BigStep (.assign name value) state (Function.update state name (value.eval state))
  | seq {first second initial middle final}
      (firstStep : BigStep first initial middle)
      (secondStep : BigStep second middle final) :
      BigStep (.seq first second) initial final
  | iteTrue {guard thenBranch elseBranch initial final}
      (guardTrue : guard.eval initial = true)
      (branchStep : BigStep thenBranch initial final) :
      BigStep (.ite guard thenBranch elseBranch) initial final
  | iteFalse {guard thenBranch elseBranch initial final}
      (guardFalse : guard.eval initial = false)
      (branchStep : BigStep elseBranch initial final) :
      BigStep (.ite guard thenBranch elseBranch) initial final
  | whileFalse {guard body state}
      (guardFalse : guard.eval state = false) :
      BigStep (.while guard body) state state
  | whileTrue {guard body initial middle final}
      (guardTrue : guard.eval initial = true)
      (bodyStep : BigStep body initial middle)
      (loopStep : BigStep (.while guard body) middle final) :
      BigStep (.while guard body) initial final

Uses 6 · Used by 38

Statement usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Commands of IMP · IMP program states

Used byCounted loop runs are big-step executions · Relative completeness of total-correctness Hoare logic · Total-correctness Hoare logic is relatively complete · Uniqueness of the loop iteration count · Partial-correctness Hoare logic matches the denotational semantics · The weakest liberal precondition gives a derivable triple · Every terminating loop run has an iteration count · Loop invariants entail the weakest liberal precondition of the loop · Loop runs with a given number of iterations · The iteration count of a nonterminating loop is zero · Total-correctness weakest precondition implies the weakest liberal precondition · Soundness of Hoare logic for partial correctness · Soundness of total-correctness Hoare logic · Total-correctness Hoare logic is sound and complete for the denotational semantics · The weakest-precondition triple is derivable in total-correctness Hoare logic · Total correctness gives a terminating small-step run · 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 · Correctness of compilation to the stack machine · Compiled command code simulates big-step execution · Denotational executions are big-step executions · Big-step executions are denotational executions · The denotational semantics of IMP is deterministic · Agreement of the denotational and big-step semantics of IMP · Determinism of IMP big-step semantics · Hoare validity via small-step termination · Big-step executions terminate in small steps · Prepending one small step to a big-step execution · Prepending finitely many small steps to a big-step execution · Small-step termination implies big-step evaluation · Equivalence of small-step and big-step semantics

TheoremDeterminism of IMP big-step semantics#✓fully proved

For every command \(c\) and every state \(s\), if \(c\) run from \(s\) terminates in a state \(t_1\) and also in a state \(t_2\) under the big-step semantics, then \(t_1 = t_2\).

theorem deterministic {command : Cmd} {initial firstFinal secondFinal : State}
    (first : BigStep command initial firstFinal)
    (second : BigStep command initial secondFinal) :
    firstFinal = secondFinal

Uses 7 · Used by 5

Statement usesBig-step semantics of IMP · Commands of IMP · IMP program states

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

Used byUniqueness of the loop iteration count · Total-correctness weakest precondition implies the weakest liberal precondition · Total correctness implies partial correctness · The denotational semantics of IMP is deterministic · Small-step termination is deterministic

AbbreviationIMP configuration#✓fully proved

A configuration of IMP is a pair \((c, \sigma)\) of a command \(c\) and a state \(\sigma\).

abbrev Config := Cmd × State

Uses 2 · Used by 10

Statement usesCommands of IMP · IMP program states

Used byExecutions of embedded commands are plain executions · Embedded plain commands are safe · Heap steps of embedded commands are plain steps · Plain executions lift to the heap language · Determinism of IMP small-step semantics · Big-step executions terminate in small steps · Prepending one small step to a big-step execution · Prepending finitely many small steps to a big-step execution · IMP small-step relation · IMP multi-step relation

InductiveIMP small-step relation#✓fully proved

The single-step relation \(\to\) on IMP configurations is the smallest relation satisfying the following rules, for all variables \(x\), arithmetic expressions \(a\), Boolean expressions \(b\), commands \(c, c_1, c_1', c_2\) and states \(\sigma, \sigma'\). Assignment: \((x := a, \sigma) \to (\mathtt{skip}, \sigma[x \mapsto v])\), where \(v\) is the value of \(a\) in \(\sigma\). Sequencing: \((\mathtt{skip}; c_2, \sigma) \to (c_2, \sigma)\), and if \((c_1, \sigma) \to (c_1', \sigma')\) then \((c_1; c_2, \sigma) \to (c_1'; c_2, \sigma')\). Conditional: \((\mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2, \sigma)\) steps to \((c_1, \sigma)\) if \(b\) evaluates to true in \(\sigma\) and to \((c_2, \sigma)\) if it evaluates to false. Loop: \((\mathtt{while}\ b\ \mathtt{do}\ c, \sigma)\) steps to \((W, \sigma)\), where \(W\) is the command \(\mathtt{if}\ b\ \mathtt{then}\ (c; \mathtt{while}\ b\ \mathtt{do}\ c)\) \(\mathtt{else}\ \mathtt{skip}\).

Cslib.IMP.Step · 18 lines

inductive Step : Config → Config → Prop
  | assign (state) (name) (value) :
      Step (.assign name value, state)
        (.skip, Function.update state name (value.eval state))
  | seqSkip (second) (state) :
      Step (.seq .skip second, state) (second, state)
  | seqStep {first first' second initial final}
      (step : Step (first, initial) (first', final)) :
      Step (.seq first second, initial) (.seq first' second, final)
  | iteTrue {guard thenBranch elseBranch state}
      (guardTrue : guard.eval state = true) :
      Step (.ite guard thenBranch elseBranch, state) (thenBranch, state)
  | iteFalse {guard thenBranch elseBranch state}
      (guardFalse : guard.eval state = false) :
      Step (.ite guard thenBranch elseBranch, state) (elseBranch, state)
  | whileStep (guard) (body) (state) :
      Step (.while guard body, state)
        (.ite guard (.seq body (.while guard body)) .skip, state)

Uses 7 · Used by 9

Statement usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Commands of IMP · IMP configuration · IMP program states

Used byExecutions of embedded commands are plain executions · Embedded plain commands are safe · Heap steps of embedded commands are plain steps · Plain executions lift to the heap language · Determinism of IMP small-step semantics · Big-step executions terminate in small steps · Prepending one small step to a big-step execution · Prepending finitely many small steps to a big-step execution · IMP multi-step relation

AbbreviationIMP multi-step relation#✓fully proved

The relation \(\to^*\) on IMP configurations is the reflexive, transitive closure of the small-step relation: \(x \to^* y\) when \(y\) is reached from \(x\) by a finite sequence of zero or more small steps.

abbrev Steps : Config → Config → Prop := Relation.ReflTransGen Step

Uses 2 · Used by 8

Statement usesIMP configuration · IMP small-step relation

Used byHoare validity embeds into separation validity · Executions of embedded commands are plain executions · Embedded plain commands are safe · Embedding preserves termination · Plain executions lift to the heap language · Big-step executions terminate in small steps · Prepending finitely many small steps to a big-step execution · Termination of an IMP command

DefinitionTermination of an IMP command#✓fully proved

A command \(c\) terminates from an initial state \(\sigma\) in a final state \(\tau\) when the configuration \((c, \sigma)\) reaches \((\mathtt{skip}, \tau)\) in finitely many small steps.

def Terminates (command : Cmd) (initial final : State) : Prop :=
  Steps (command, initial) (.skip, final)

Uses 3 · Used by 8

Statement usesCommands of IMP · IMP program states · IMP multi-step relation

Used byTotal correctness gives a terminating small-step run · Hoare validity embeds into separation validity · Embedding preserves termination · Small-step termination is deterministic · Hoare validity via small-step termination · Big-step executions terminate in small steps · Small-step termination implies big-step evaluation · Equivalence of small-step and big-step semantics

TheoremDeterminism of IMP small-step semantics#✓fully proved

For all IMP configurations \(x\), \(y\), \(z\), if \(x\) steps to \(y\) and \(x\) steps to \(z\) in one small step, then \(y = z\).

theorem deterministic {x y z : Config} (h1 : Step x y) (h2 : Step x z) : y = z

Uses 8

Statement usesIMP configuration · IMP small-step relation

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

TheoremBig-step executions terminate in small steps#✓fully proved

For every IMP command \(c\) and states \(s\) and \(s'\), if \(c\) evaluates from \(s\) to \(s'\) in the big-step semantics, then \(c\) started in \(s\) terminates by small steps in \(s'\): finitely many small steps lead from the configuration \((c, s)\) to \((\mathrm{skip}, s')\).

theorem Terminates.of_bigStep {c : Cmd} {s s' : State} (h : BigStep c s s') :
    Terminates c s s'

Uses 11 · Used by 2

Statement usesBig-step semantics of IMP · Commands of IMP · IMP program states · Termination of an IMP command

Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · IMP configuration · IMP small-step relation · IMP multi-step relation

Used byHoare validity via small-step termination · Equivalence of small-step and big-step semantics

TheoremPrepending one small step to a big-step execution#✓fully proved

Let \(x = (c, s)\) and \(y = (d, t)\) be configurations and \(s'\) a state. If \(x\) moves to \(y\) in one small step and \(d\) evaluates from \(t\) to \(s'\) in the big-step semantics, then \(c\) evaluates from \(s\) to \(s'\) in the big-step semantics.

theorem BigStep.of_step {x y : Config} {s' : State} (hstep : Step x y)
    (h : BigStep y.1 y.2 s') : BigStep x.1 x.2 s'

Uses 9 · Used by 1

Statement usesBig-step semantics of IMP · Commands of IMP · IMP configuration · IMP program states · IMP small-step relation

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

Used byPrepending finitely many small steps to a big-step execution

TheoremPrepending finitely many small steps to a big-step execution#✓fully proved

Let \(x = (c, s)\) and \(y = (d, t)\) be configurations and \(s'\) a state. If \(x\) reaches \(y\) in finitely many (possibly zero) small steps and \(d\) evaluates from \(t\) to \(s'\) in the big-step semantics, then \(c\) evaluates from \(s\) to \(s'\) in the big-step semantics.

theorem BigStep.of_steps {x y : Config} {s' : State} (hsteps : Steps x y)
    (h : BigStep y.1 y.2 s') : BigStep x.1 x.2 s'

Uses 7 · Used by 1

Statement usesBig-step semantics of IMP · Commands of IMP · IMP configuration · IMP program states · IMP multi-step relation

Proof usesPrepending one small step to a big-step execution · IMP small-step relation

Used bySmall-step termination implies big-step evaluation

TheoremSmall-step termination implies big-step evaluation#✓fully proved

For every IMP command \(c\) and states \(s\) and \(s'\), if \(c\) started in \(s\) terminates by small steps in \(s'\), then \(c\) evaluates from \(s\) to \(s'\) in the big-step semantics.

theorem BigStep.of_terminates {c : Cmd} {s s' : State} (h : Terminates c s s') :
    BigStep c s s'

Uses 5 · Used by 3

Statement usesBig-step semantics of IMP · Commands of IMP · IMP program states · Termination of an IMP command

Proof usesPrepending finitely many small steps to a big-step execution

Used bySmall-step termination is deterministic · Hoare validity via small-step termination · Equivalence of small-step and big-step semantics

TheoremEquivalence of small-step and big-step semantics#✓fully proved

For every IMP command \(c\) and states \(s\) and \(s'\), \(c\) started in \(s\) terminates by small steps in \(s'\) if and only if \(c\) evaluates from \(s\) to \(s'\) in the big-step semantics.

theorem terminates_iff_bigStep {c : Cmd} {s s' : State} :
    Terminates c s s' ↔ BigStep c s s'

Uses 6 · Used by 1

Statement usesBig-step semantics of IMP · Commands of IMP · IMP program states · Termination of an IMP command

Proof usesSmall-step termination implies big-step evaluation · Big-step executions terminate in small steps

Used byTotal correctness gives a terminating small-step run

TheoremSmall-step termination is deterministic#✓fully proved

For every IMP command \(c\) and states \(s\), \(s_1\), \(s_2\), if \(c\) started in \(s\) terminates by small steps in \(s_1\) and also terminates by small steps in \(s_2\), then \(s_1 = s_2\).

theorem Terminates.deterministic {c : Cmd} {s s1 s2 : State}
    (h1 : Terminates c s s1) (h2 : Terminates c s s2) : s1 = s2

Uses 5

Statement usesCommands of IMP · IMP program states · Termination of an IMP command

Proof usesDeterminism of IMP big-step semantics · Small-step termination implies big-step evaluation

TheoremHoare validity via small-step termination#✓fully proved

For assertions \(P\) and \(Q\) on states and an IMP command \(c\), the partial-correctness Hoare triple with precondition \(P\), command \(c\) and postcondition \(Q\) is valid if and only if, for all states \(s\) and \(s'\), whenever \(P\) holds in \(s\) and \(c\) started in \(s\) terminates by small steps in \(s'\), \(Q\) holds in \(s'\).

theorem Valid.iff_terminates {pre post : Assertion} {c : Cmd} :
    Valid pre c post ↔
      ∀ ⦃s s' : State⦄, pre s → Terminates c s s' → post s'

Uses 8 · Used by 1

Statement usesAssertion · Commands of IMP · IMP program states · Termination of an IMP command · Validity of a Hoare triple

Proof usesBig-step semantics of IMP · Small-step termination implies big-step evaluation · Big-step executions terminate in small steps

Used byHoare validity embeds into separation validity

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.