Definition 7.1.1. Specification, semantically.
A specification \(S\subseteq\Sigma\times\Sigma\) is a set of pairs of states.
Section 7.1 Functional Correctness
What does it mean if we say that a program is correct? First, there may be different criteria of correctness: The program delivers its results in a certain time budget, which is very important in real-time systems 14 or does only consume a certain amount of memory or does not exhibit certain security problems (e.g. side channels). Most important however is functional correctness. By functional correctness, we mean that the program computes what it is supposed to compute. But how to we declare what is the right thing to compute? To this end, we need a specification.
The idea of this definition is that a specification relates starting states with terminating states of program executions. Each pair in the set of a semantical specification basically says: If you start executing the program in the first state of the pair, program execution shall end in the second state of the pair.
For example, the following specification specifies that variable \(\CVar y\) has the value \(\CVar x+1\) in the final state.
\begin{equation*}
S_\text{add}=\{(\sigma,\sigma')\mid \sigma'\,\CVar y=\sigma\,\CVar x+1\}
\end{equation*}
Let us consider the specification \(S_\text{max}\) of the computation of the maximum of two variables \(\CVar x\) and \(\CVar y\text{.}\) It is given by the following set of state pairs:
\begin{align*}
S_\text{max} = \amp \{(\{\CVar x\mapsto 1, \CVar y\mapsto 1\}, \{\CVar x\mapsto 1, \CVar y\mapsto 1,\CVar m\mapsto 1\}), \\
\amp (\{\CVar x\mapsto 1, \CVar y\mapsto 2\}, \{\CVar x\mapsto 1, \CVar y\mapsto 2,\CVar m\mapsto 2\}), \\
\amp \vdots \\
\amp (\{\CVar x\mapsto 42, \CVar y\mapsto 37\}, \{\CVar x\mapsto 42, \CVar y\mapsto 37,\CVar m\mapsto 42\}), \\
\amp \vdots
\end{align*}
or more compact:
\begin{equation}
S_\text{max}=\{(\sigma,\sigma')\mid\sigma'\,\CVar m\ge\sigma\,\CVar x\land\sigma'\,\CVar m\ge\sigma\,\CVar y\land(\sigma'\,\CVar m=\sigma\,\CVar x\lor\sigma'\,\CVar m=\sigma\,\CVar y)\}\tag{7.1}
\end{equation}
Ultimately, we want to document the specification of a program in the program text itself. So, writing down specifications on the semantical level (i.e. by directly referring to states) is not appropriate because states are not an element of the syntax of a program but its semantics. Therefore, it is common practice to use assertions to express constraints on states at a particular program point and use them to express specifications.
Definition 7.1.2. Assertion.
An assertion \(a\) is a logical formula over the expression language of the programming language. In the following, we will discuss assertions in the context of C0 and define assertions here using the following syntax definition (for the sake of brevity, we only give concrete syntax):
\begin{equation*}
\Assert\ni A\syndef e\mid\ltrue\mid\lfalse\mid\lneg A\mid A_1\land A_2\mid A_1\lor A_2\mid A_1\limp A_2\mid A_1\liff A_2\mid \forall x.A\mid\exists x.A
\end{equation*}
where operators more to the left bind stronger. Note that \(e\in\Expr\) is a C0 expression.
Definition 7.1.2 defines assertions as logical formulas of first-order logic over the C0 expression language. After defining the syntactic structure of an assertion, let us define which set of states is actually described by an assertion. To this end, we define the notion of a model of an assertion.
Definition 7.1.3. Model.
A state \(\sigma\) is a model of an assertion \(A\) if it satisfies \(A\text{.}\) Satisfaction is defined by the relation \(\models\) which is defined inductively on the assertion language:
\begin{align*}
\sigma \amp \models e \amp\amp\text{iff }\denotR{e}\sigma\ne 0\\
\sigma \amp \models \lneg A \amp\amp\text{iff }\sigma\not\models A\\
\sigma \amp \models A_1\land A_2 \amp\amp\text{iff }\sigma\models A_1\text{ and }\sigma\models A_2\\
\sigma \amp \models \forall x.A \amp\amp\text{iff for every }i\in\mathtt{int}\text{ there is }\sigma[i/x]\models A
\end{align*}
All the other operators in \(\mathit{Assert}\) are just syntactical sugar
\begin{align*}
\lfalse\amp =x\land\lneg x \amp \ltrue\amp =\lneg\lfalse\\
A_1\lor A_2\amp=\lneg(\lneg A_1\land\lneg A_2) \amp A_1\limp A_2\amp=\lneg A_1\lor A_2\\
A_1\liff A_2\amp = (A_1\limp A_2)\land(A_2\limp A_1)\amp \exists x.A \amp=\neg\forall x.\lneg A
\end{align*}
and \(\models\) is defined on them accordingly.
Definition 7.1.4. Satisfiability and Validity.
We say an assertion \(A\) is
- satisfiable if it has some model.
- unsatisfiable if it has no model.
- valid if every state is a model of \(A\) which is equivalent to saying that \(\lneg A\) is unsatisfiable.
- not valid if there is a state that is not a model of \(A\) which is equivalent to \(\lneg A\) is satisfiable.
We will now use the assertion language we defined and express specifications syntactically by means of a precondition and a postcondition.
Definition 7.1.5. Specification, syntactically.
A pair of assertions \((P,Q)\) is called a specification. In such a specification, \(P\) is called precondition and \(Q\) is called postcondition.
For example, the assertions
\begin{equation}
P=\ltrue\qquad Q=\CVar m\ge\CVar x\land\CVar m\ge\CVar y\land(\CVar m=\CVar x\lor\CVar m=\CVar y)\tag{7.2}
\end{equation}
constitute a specification for a program that computes the maximum of \(\CVar x\) and \(\CVar y\text{.}\)
When looking at the semantical (7.1) and syntactical (7.2) specifications for the maximum program, one observes that the semantical specification draws a connection from the starting state to the final state of an execution, e.g. by stating that \(\sigma'\,\CVar m\ge\sigma\ \CVar x\text{:}\) both, \(\sigma\) and \(\sigma'\) appear in (7.1). This is not the case for the syntactical specification that merely consists of two assertions.
So, in principle, the syntactical specification is weaker and admits programs like the following:
x = 1;
y = 2;
m = y;
This is not a problem if we are just interested in verifying a given program with respect to a specification. However, if we are interested in synthesis, i.e. creating programs that are correct with respect to a given specification, this plays a role. We then need additional constraints outside of the specification such as demanding that the program we are looking for does not modify its inputs.
One way of achieving this is introducing ghost variables that capture the initial values of all variables in the program but are forbidden to be modified by the program itself. We denote the ghost variables here with capital letters.
Using ghost variables, we can refine the specification of programs that compute the maximum of two values such that the result variable \(\CVar m\) contains the maximum of values of \(\CVar x\) and \(\CVar y\) at the start of the program.
\begin{equation}
P=\CVar X=\CVar x\land\CVar Y=\CVar y\qquad Q=\CVar m\ge\CVar X\land\CVar m\ge\CVar Y\land(\CVar m=\CVar X\lor\CVar m=\CVar Y)\tag{7.3}
\end{equation}
Now, we can use our notion of a specification and define what it means for a program to be correct. We do this by leveraging our formal notion of program semantics that we have developed in Chapter 6 and link it to the formal notion of specifications we developed above.
Definition 7.1.6. Total Correctness.
A program \(p\) is totally correct with respect to a specification \((P,Q)\) if for every model \(\sigma\) of \(P\) there is a model \(\sigma'\) of \(Q\) such that \(\config p\sigma\) properly terminates 6.3.7 in \(\sigma'\text{.}\) More formally:
\begin{equation*}
(\sigma\models P)\limp\left(\exists\sigma'.\config p\sigma\terminates\configt{\sigma'}\land\sigma'\models Q\right)
\end{equation*}
It is customary to write the statement “Program \(p\) is totally correct with respect to the specification \((P,Q)\)” using a so-called Hoare triple 15 \(\hoaret PpQ\)
Note that if a program gets stuck or aborts on a state that satisfies the precondition, the program is not totally correct.
Reasoning about total correctness implies reasoning about program termination as well: If we want to prove a program totally correct, we have to implicitly also prove that it terminates on all states that satisfy the precondition. This is sometimes a bit too heavy and therefore one often uses the notion of partial correctness in practice, where reasoning about termination is left out.
Definition 7.1.7. Partial Correctness.
A program \(p\) is partially correct with respect to a specification \((P,Q)\) if for every model \(\sigma\) of \(P\) it either properly terminates in a state \(\sigma'\) that satisfies \(Q\) or diverges. More formally:
\begin{equation*}
(\sigma\models P)\limp\left(\forall p'~\sigma'.\config p\sigma\terminates\config {p'}{\sigma'}\limp(p'=\varepsilon\land \sigma'\models Q)\right)
\end{equation*}
We use the notation \(\hoare PpQ\) to denote partial correctness.
Note that, alike total correctness, if a program gets stuck or aborts on a state that satisfies the precondition, it is not partial correct.
Consider Figure 7.1.8. The red program is neither partially nor totally correct because it terminates in a state that does not satisfy the postcondition. The blue program is not totally correct because it is not properly terminating in a state for one input. But it is partially correct, because the properly terminating executions end in states that satisfy the postcondition. The black program is totally and partially correct although there is an execution that aborts. This execution however starts in a state that does not fulfill the precondition.
think of the software that causes your airbag to unfold.
Named after its inventor Tony Hoare. Initially, Hoare used a different notation and considered only partial correctness.
