Formulas for Representing Sets and Relations
Let the state of programs be where .
In Hoare Logic Basics we defined meaning of Hoare triple when
We also defined the meaning of wp and sp. We next look at these notions when
- are formulas defining the set of states
- command instead of relation is used to specify the program
Example: Precondition , command , postcondition . Initial state has values of x,y equal to . Relation transforms e.g. into etc. Previously we worked on such sets and relations. Today we work on actual formulas i.e. their syntax trees.
Let and be formulas in our language and a command, following the syntax of our simple programming language.
We define Hoare triples on these syntactic entities by taking their interpretation as sets and relations. Specifically, given definitions in the Hoare Logic Basics, we define
- = (informally) =
- = (informally) =
- is the meaning of relation given by Relational Semantics
Taking into account the definition of Hoare triple for sets and relation , we conclude that is equivalent to
We similarly extend the notion of and to work on formulas and commands.
We use the same notation and infer from the context whether we are dealing with sets and relations or formulas and commands.
To express condition , we will compute formulas that define relations, following the definition of from Relational Semantics.
Formulas That Specify Relations
To specify relation we compute by formula containing specifying the semantics of c_1, that is, formula such that, informally,
Note that above
- denotes the initial state
- denotes the final state of the command.
Denote the truth value of formula in two states by :
We can then write more precisely the condition for formula . It should be formula such that:
We thus have
With such notion of , we represent the validity of a Hoare triple with
as the validity of the formula:
We next give rules for computing for each (loop-free) command .