Skip to main content

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.

Definition 7.1.1. Specification, semantically.

A specification \(S\subseteq\Sigma\times\Sigma\) is a set of pairs of states.

The idea of this definition is that a specification relates starting with terminating states of program executions. To this end, it captures pairs of input and output It captures pairs input and output pairs both given as states.

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 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.

We defined assertions to be formulas of first-order logics (also known as predicate logics).

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{.}\)

Remark 7.1.6.

When looking at the semantical (7.1) and syntactical (7.2) specifications for the maximum program very closely, one observes that the semantical specification really 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 correct programs from 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.

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.7. Total Correctness.

A program \(s\) 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 s\sigma\) properly terminates 6.3.8 in \(\sigma'\text{.}\) More formally:

\begin{equation*} (\sigma\models P)\limp\left(\exists\sigma'.\config s\sigma\terminates\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 PsQ\)

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.8. Partial Correctness.

A program \(s\) 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 c.\config s\sigma\terminates c\limp(c=\sigma'\land\sigma'\models Q)\right) \end{equation*}

We use the notation \(\hoare PsQ\) 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.

Figure 7.1.9. The set of all states before and after the execution of \(s\text{.}\) The circle labelled \(P\) denotes all states that satisfy the precondition \(P\text{.}\) Similarly, the circle labelled \(Q\) denotes all states that satisfy the postcondition \(Q\text{.}\) The colors denote different programs and the squiggly lines denote all executions of the program with respect to the particular color.

Consider Figure 7.1.9. 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.

We will come to Hoare logical in the context of formal verification in Section 7.4.

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.