Hoare Triples
This module is a review of Hoare triples.
A Hoare triple
has the form \(\{P\} c \{Q\}\) where \(P\) and \(Q\) are predicates on
states of a system and \(c\) is a command. The meaning of the
triple is that if \(P\) holds when the command \(c\) is initiated
then execution of the command terminates and \(Q\) holds upon
termination.
\(P\) is called the
precondition and \(Q\) the
postcondition of the triple.
We assume
total
rather than partial correctness.
Examples
Examples of Hoare triples for the assignment statement \(x := x+1\)
are:
\(
\{x = 0\} \; x := x+1 \; \{x = 1\}
\)
\(
\{x = 0\} \; x := x+1 \; \{x > 0\}
\)
and:
\(
\forall k: \quad \{x = k\} \; x := x+1 \; \{x = k+1\}
\)
Variables not in the Hoare Triple
Variables that are not mentioned in a Hoare triple are assumed,
implicitly, to remain unchanged by the command. For example, if a
program has variables \(x\) and \(y\), then the triple:
\(
\{x = 0\} \; x := x+1 \; \{x = 1\}
\)
is implicitly equivalent to:
\(
\forall k: \quad \{(x = 0) \wedge (y=k) \} \; x := x+1 \; \{(x = 1)
\wedge (y = k)\}
\)
While designing a program we may specify a command in terms of its
pre- and post-conditions and later implement the command in a
programming language.
Review
- What is a Hoare triple?
- What are preconditions and postconditions of a command?
K. Mani Chandy,
Emeritus Simon Ramo Professor,
California Institute of Technology