CS 245 — Lecture 19

Introduction to Verification

At this point, if this were a mathematical logic course, we'd spend more time really proving things like soundness and completeness of first-order logic and the consequences of those results. Instead, we will try to apply some of the things we've done to verification.

There are a few approaches to this. In the textbook, there are four chapters after the chapter on predicate logic which deal with different applications of logic to verification. Things like model checking, which relies on an extension of first-order logic to something called linear temporal logic, are interesting but we only have two weeks or so to cover some material. We will focus on program verification.

Program verification is the idea that we can formally prove or verify the correctness of a program. This is in contrast to testing, where we try running programs on a small set of inputs which we hope will capture the entire behaviour of a program. Looking at this from the mathematical perspective, it is the equivalent of the classic joke about engineers proving theorems by example. Of course, that joke is not quite as funny when we realize that this is exactly how we convince ourselves that our software really works.

Formal verification involves a formal description of a specification, followed with a proof that the program satisfies the specification. Here, we can already apply our logic lens to this scenario. The formal specification acts as our premises. If the premises "work" and our proof system is sound, then we should be able to show that a program is correct and runs as intended. If the specification is flawed or our proof system is not sound, then we will have problems with this approach.

Hoare Logic

We will define and work with a formal proof system for proving that programs are correct called Hoare logic, named for C.A.R. (Tony) Hoare, who developed it in 1969. You may recognize Hoare more as the inventor of Quicksort. Much like what we have done earlier, we are applying the notion that we can define a proof system that is purely syntactic to prove the correctness of the semantics of a program. Our proof system will be defined over a "core language" which is intended to resemble popular C-like imperative programming languages.

Our language will consist of

• integer and boolean expressions
• assignment
• conditional statements
• loops
• arrays
• functions and procedures

Since we won't exhaustively define our language and rely on your intuition on what one of these things might look like, here is an example of what one of our programs might look like.

y = 1;
z = 0;
while (z != x) {
    z = z+1;
    y = y*z;
}

Since our language is imperative, when we think of the execution of a program, the program will manipulate variables and execute statements based on those variables. We consider the setting of those variables at a particular point in the execution of that program to be the state of the program at that point.

Definition 19.1. The state of a program at a given moment is the list of the values of each of its variables at that moment.

If we want to translate this to logic-world, we can think of the state as an environment. Each statement or command that we use in our program will manipulate the state in some way and it is this manipulation that defines the semantics of each command in our programming language. Again, we won't explicitly define this and defer to our expectations of what these would do in a real programming language.

Ultimately, we want to talk about the state of a program before we execute it and the state after we execute it. We will introduce some notation.

Definition 19.2. A Hoare triple is a triple $\llparenthesis \varphi \rrparenthesis P \llparenthesis \psi \rrparenthesis$ composed of

• a predicate formula $\varphi$, called a precondition,
• a program $P$, and
• a predicate formula $\psi$ called a postcondition.

Informally, we would like that if we run the program $P$, starting in a state that satisfies $\varphi$, then the resulting state will satisfy $\psi$.

Remark. The slides often use $\llparenthesis P \rrparenthesis C \llparenthesis Q \rrparenthesis$, where $P$ is a precondition, $C$ is the program, and $Q$ is the postcondition. I personally like using $\varphi$, $P$, and $\psi$ because it makes it clear the pre- and post-conditions are formulas and I like using $P$ for program rather than $C$ for code.

Note that in order to say anything useful about the programs, we will be assuming a language and interpretation for our formulas. We will be making use of the standard mathematical operators, such as < and =, - and + and *, and so on and their interpretations will be the standard mathematical interpretation for those predicates and functions.

We will use Hoare triples to specify conditions for the exeuction of our program. This is where translating conditions about software into formal logical expressions becomes important. Note that by definition, a Hoare triple is any $\varphi$, $P$, and $\psi$ with the funny brackets $\llparenthesis$ and $\rrparenthesis$. In other words, the definition of a Hoare triple is a synatctic definition and there's nothing saying that a Hoare triple has to be correct. Obviously, it would be ideal if all software specifications had to be correct, but clearly, they do not have to be.

Definition 19.3. A specification of a program $P$ is a Hoare triple with $P$ as the middle element of the triple.

Example 19.4. The specification of an integer square root program might be $$\llparenthesis x \geq 0 \rrparenthesis P \llparenthesis y \times y \leq x \rrparenthesis.$$ However, this specification is not quite good enough. For instance, if we take our program $P$ to be y = 0;, then $P$ satisfies our specification. Something better would be $$\llparenthesis x \geq 0 \rrparenthesis P \llparenthesis (y \times y \leq x) \wedge (\forall z ((z \times z \leq x ) \rightarrow (z \leq y))) \rrparenthesis.$$ This specification would be satisfied by the program

y = 0;
while (y*y <= x) {
    y = y+1
}
y = y-1;

Example 19.5. Let's try to specifiy conditions for the following program:

y = 1;
while (x != 0) {
    y = y*x;
    x = x-1;
}

What we might want to do is have a postcondition $\llparenthesis y = x! \rrparenthesis$. However, this won't work, since $x$ changes. One way to fix this is to introduce the notion of logical variables. These are variables that aren't a part of the program and exist only for the purposes of defining specifications. So for this program, we can use the logical variable $x_0$ to define the precondition $\llparenthesis (x = x_0) \wedge (x_0 \geq 0) \rrparenthesis$ and the postcondition $\llparenthesis y = x_0! \rrparenthesis$.

Definition 19.6. For a Hoare triple $\llparenthesis \varphi \rrparenthesis P \llparenthesis \psi \rrparenthesis$, its set of logical variables are those variables that are free in $\varphi$ or $\psi$ and do not occur in $P$.

A proof system for partial correctness

Once we have a specification, we need to talk about when we can consider that specification to be satisfied. From the definitions, that we've already seen, such a definition (almost) follows quite naturally.

Definition 19.7. A Hoare triple is satisfied under partial correctness if, whenever execution starts in a state satisfying precondition $\varphi$, and terminates, it follows that the state after execution satisfies postcondition $\psi$. We denote partial correctness by $$\vdash_{par} \llparenthesis \varphi \rrparenthesis P \llparenthesis \psi \rrparenthesis.$$

Example 19.8. The Hoare triple $\llparenthesis x = x_0 \rrparenthesis$ x = 1; $\llparenthesis x = 1 \rrparenthesis$ is satisfied under partial correctness. On the other hand, the Hoare triple $\llparenthesis x = x_0 \rrparenthesis$ x = 0; $\llparenthesis x = 1 \rrparenthesis$ is not satisfied under partial correctness.

Note here that we define partial correctness, which seems to imply the existence of something stronger, like perhaps maybe something like total correctness. This will be important later on. However, for a quick example of why this doesn't completely capture our intuitive understanding of what it means to satisfy a triple, consider the following program:

while true {x = 0;}

If we set $P$ to be this program, then every specification for $P$ will be satisfied under partial correctness (why?).

We will now develop a proof system for validating Hoare triples. We would like to show that a program is correct. However, we will inevitably run into programs like the infinite while loop we saw earlier. So for now, we will only focus on showing partial correctness with our proof system. We will now describe the rules in our proof system and how to apply them to the structure of a program.

Up until now, we have been applying rules on an entire program. The first rule, composition, is important for describing how to propagate conditions throughout the program. This will also describe the structure of a proof of a program.

Definition 19.9. The rule for composition is: $$\frac{\llparenthesis \varphi \rrparenthesis C_1 \llparenthesis \eta \rrparenthesis \quad \llparenthesis \eta \rrparenthesis C_2 \llparenthesis \psi \rrparenthesis }{\llparenthesis \varphi \rrparenthesis C_1; C_2 \llparenthesis \psi \rrparenthesis} \text{(composition)}$$

This says that in order to prove $\llparenthesis \varphi \rrparenthesis C_1; C_2 \llparenthesis \psi \rrparenthesis$, we need to find a midcondition $\eta$ and prove $\llparenthesis \varphi \rrparenthesis C_1 \llparenthesis \eta \rrparenthesis$ and $\llparenthesis \eta \rrparenthesis C_2 \llparenthesis \psi \rrparenthesis$.

We can use this to talk about what a proof in this proof system might look like. We begin with a precondition for our entire program and end with a postcondition for our program, but what do the steps in between look like? We can consider each statement to be a program of its own with its own preconditions and postconditions. Then the postcondition of one statement becomes the precondition of the statement immediately following it.

More formally, what this looks like is if we want to prove $\vdash_{par} \llparenthesis \varphi_0 \rrparenthesis C_1; C_2; \dots ; C_n \llparenthesis \varphi_n \rrparenthesis$, we compose the proofs of $\vdash_{par} \llparenthesis \varphi_i \rrparenthesis C_{i+1} \llparenthesis \varphi_{i+1} \rrparenthesis$ for $i = 0, 1, \dots, n-1$ to get

What we get is something that resembles an excessively commented piece of code:

    y = y * x; 

    x = x - 1; 

When writing a proof, we typically know the precondition and postcondition already and provide the midconditions as part of the proof. We will see that because our programming language is heavily assignment-based, it is usually easier to work backwards. The reason for this is because of the way the next rule, assignment works. Since our language is very heavily based on manipulating state, this is quite important.

Definition 19.10 The assignment rule is: $$\frac{}{\llparenthesis \psi[E/x] \rrparenthesis x = E \llparenthesis \psi \rrparenthesis} \text{(assignment)}$$

Note that the assignment rule has no premises.

Example 19.11. $$\vdash_{par} \llparenthesis y + 1 = 7 \rrparenthesis x = y + 1 \llparenthesis x = 7 \rrparenthesis$$ Alternatively, we can write this as

Observe that the assignment rule is defined so that the precondition is a substitution of the postcondition. This is kind of like the rule $\exists$i from predicate logic, where it is helpful to think about how the rule works in reverse. This is the reason that we tend to work backwards when filling in a verification proof.

Just as with the $\exists$i rule, this seems counter-intuitive at first, since we think about substitution and assignment in the forward direction. However, we have to remember that in verification, what we are considering is the conditions that we would like our program to obey.

When an assignment x = E is executed, we likely want $\psi$ to say something about the value of $x$, which just got assigned. But this means that what we want to say about $x$, we would be saying about $E$ before the assignment occurs. In this sense, we should be able to take what we want to say about $x$, replace $x$ with $E$, and it should also hold before the assignment. Hence, we get $\psi[E/x]$.

Definition 19.12. The following rule, called implied can be split up into a set of two rules: $$\frac{(\varphi \rightarrow \varphi') \quad \llparenthesis \varphi' \rrparenthesis P \llparenthesis \psi \rrparenthesis}{\llparenthesis \varphi \rrparenthesis P \llparenthesis \psi \rrparenthesis} \quad \frac{\llparenthesis \varphi \rrparenthesis P \llparenthesis \psi' \rrparenthesis \quad (\psi' \rightarrow \psi)}{\llparenthesis \varphi \rrparenthesis P \llparenthesis \psi \rrparenthesis}\text{(implied)}$$

Both of these has a different name. The first, where we have $(\varphi \rightarrow \varphi')$ is called precondition strengthening. This means that $\varphi$ is a stronger precondition than $\varphi'$. The second, where $(\psi' \rightarrow \psi)$ is called postcondition weakening, which means that $\psi$ is a weaker postcondition than $\psi'$. These rules are sometimes necessary to adjust formulas for use with other applications of rules.

If we wanted to be very formal, we could require that in order to conclude one of the implications, like $(\varphi \rightarrow \varphi')$, we must provide a proof of $\varphi \vdash \varphi'$. We will not do that but this means that you should make sure not to accidentally imply something that isn't true.

Example 19.13. While composition is clearly implicit in a proof like the following, we should not implicitly perform precondition strengthening or postcondition weakening. As mentioned above, one can certainly prove that $(((x = x_0) \wedge (y = y_0)) \rightarrow ((y = y_0) \wedge (x = x_0)))$, but it isn't required.

Example 19.14. In the following example, we have an implication from $\texttt T$, or true. Equality is also something that isn't too hard to prove if we have the right machinery (for example, see Assignment 9, Question 4).