LARA

Formulas for Representing Sets and Relations

Let the state of programs be $S = (V \to \mathbb{Z})$ where $V = \{x_1,\ldots,x_n\}$.

In Hoare Logic Basics we defined meaning of Hoare triple $\{P\}r_1\{Q\}$ when

  • $P,Q \subseteq S$
  • $r_1 \subseteq S \times S$

We also defined the meaning of wp and sp. We next look at these notions when

  • $P,Q$ are formulas defining the set of states
  • command $c$ instead of relation $r$ is used to specify the program

Example: Precondition $x \ge 1 \land y \ge 2$, command $x=y+2$, postcondition $x \ge 3$. Initial state has values of x,y equal to $(1,2), (1,3),...,(2,2), (2,3),\ldots$. Relation transforms e.g. $(0,0)$ into $(2,0)$ etc. Previously we worked on such sets and relations. Today we work on actual formulas i.e. their syntax trees.

Let $P$ and $Q$ be formulas in our language $F$ and $c$ 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

\begin{equation*} \{ P \} c_1 \{ Q \} \end{equation*}

to mean

\begin{equation*} \{ P_S \} r_1 \{ Q_S \} \end{equation*}

where

Above, $f_T$ assigns a predicate to the formula according to Relational Semantics and is similar to function $e_F$ for evaluating formulas in First-order logic semantics.

Taking into account the definition of Hoare triple for sets $P',Q'$ and relation $r_1$, we conclude that $\{ P \} c_1 \{ Q \}$ is equivalent to

\begin{equation*} \forall s_1, s_2.\ f_T(P)(s_1) \land (s_1,s_2) \in r_c(c_1) \rightarrow f_T(Q)(s_2) \end{equation*}

We similarly extend the notion of $sp(P,r)$ and $wp(r,Q)$ 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 $(s_1,s_2) \in r_c(c_1)$, we will compute formulas that define relations, following the definition of $r_c$ from Relational Semantics.

Formulas That Specify Relations

To specify relation $r_c(c_1)$ we compute by formula $F$ containing $x_1,\ldots,x_n,x'_1,\ldots,x'_n$ specifying the semantics of c_1, that is, formula $F_1$ such that, informally,

\begin{equation*} r_c(c_1) = \{ (\{("x_1",x_1),\ldots,("x_n",x_n)\},\{("x_1",x'_1),\ldots,("x_n",x'_n)\}).\ F_1 \} \end{equation*}

Note that above

  • $\{("x_1",x_1),\ldots,("x_n",x_n)\}$ denotes the initial state
  • $\{("x_1",x'_1),\ldots,("x_n",x'_n)\}$ denotes the final state of the command.

Denote the truth value of formula in two states by $f_{T2}(F_1)(s,s')$:

\begin{equation*} \begin{array}{l} f_{T2}(F_1 \land F_2)(s,s') = f_{T2}(F_1)(s,s') \land f_{T2}(F_2)(s,s') \\ f_{T2}(F_1 \lor F_2)(s,s') = f_{T2}(F_1)(s,s') \lor f_{T2}(F_2)(s,s') \\ f_{T2}(\lnot F_1)(s,s') = \lnot f_{T2}(F_1)(s,s') \\ f_{T2}(t_1 = t_2)(s,s') = (f_{T2}(t_1)(s,s') = f_{T2}(t_2)(s,s')) \\ f_{T2}(t_1 < t_2)(s,s') = (f_{T2}(t_1)(s,s') < f_{T2}(t_2)(s,s')) \\ f_{T2}(t_1 + t_2)(s,s') = f_{T2}(t_1)(s,s') + f_{T2}(t_2)(s,s') \\ f_{T2}(t_1 - t_2)(s,s') = f_{T2}(t_1)(s,s') - f_{T2}(t_2)(s,s') \\ f_{T2}(K * t_1)(s,s') = K \cdot f_{T2}(t_1)(s,s') \\ f_{T2}(x)(s,s') = s(x) \\ f_{T2}(x')(s,s') = s'(x) \end{array} \end{equation*}

We can then write more precisely the condition for formula $F_c(c_1)$. It should be formula $F_1$ such that:

\begin{equation*} r_c(c_1) = \{ (s,s').\ f_{T2}(F_1)(s,s') \} \end{equation*}

We thus have

\begin{equation*} r_c(c_1) = \{ (s,s').\ f_{T2}(F_c(c_1))(s,s') \} \end{equation*}

With such notion of $F_c(c_1)$, we represent the validity of a Hoare triple with

  • precondition $P$
  • command $c_1$
  • postcondition $Q$

as the validity of the formula:

\begin{equation*} \forall \vec x,\vec x\,'.\ (P(\vec x) \land F_c(c_1)(\vec x,\vec x\,')\ \rightarrow\ Q(\vec x\,')) \end{equation*}

where

  • $\vec x$ denotes $x_1,\ldots,x_n$
  • $\vec x\,'$ denotes $x'_1,\ldots,x'_n$

We next give rules for computing $F_c(c_1)$ for each (loop-free) command $c_1$.