Definition. Hoare triple - partial correctness [003x]
Definition. Hoare triple - partial correctness [003x]
The basic unit of reasoning or judgement of the partial correctness of a program is the Hoare triple denoted as:
\[ \{P\}\ s\ \{Q\} \]where:
- \(P\) represents the precondition which must hold true before the execution of the statement \(s\).
- \(Q\) represents the postcondition which must hold true after the execution of the statement \(s\), provided that \(P\) was true before execution.
If we consider a variable state \(\sigma : \texttt {String} \to \mathbb {Z}\) mapping variable names to integer values, then we can define the partial correctness condition of a Hoare triple as follows:
\[ \sigma \vDash P \to \exists \sigma '.\ \langle s, \sigma \rangle \Downarrow \sigma ' \to \sigma ' \vDash Q \]What this says is that: if the precondition \(P\) holds in the initial state \(\sigma \), and if executing the statement \(s\) from that state leads to a new state \(\sigma '\), then the postcondition \(Q\) must hold in the new state \(\sigma '\).
In a more programmatic sense we can understand the pre and postconditions as assertions on the memory state \(\sigma \), in other words they represent a function \(A : (\texttt {String} \to \mathbb {Z}) \to \texttt {Prop}\) that evaluates to true or false based on the values of the variables in the state. Thus, we can rewrite the Hoare triple condition as:
\[ P(\sigma ) \to \exists \sigma '.\ \langle s, \sigma \rangle \Downarrow \sigma ' \to Q(\sigma ') \]Or in lean equivalently as:
abbrev Condition := Memory -> Prop
def HoareTriple {P Q : Condition} (c : Stmt) : Prop :=
∀ σ σ', P σ → (c, σ) ⇓ₛ σ' → Q σ'
A note here is that we are using some custom notation for the big-step semantics relation. The notation \(\Downarrow _s\) here simply means the big step evaluation relation for statements.
In general for a Hoare triple we denote its validity as:
\[ \vDash \{P\}\ s\ \{Q\} \]