“It may be true, that whenever C actually reaches a certain point in the flow diagram, one or more bound variables will necessarily possess certain specified values, or possess certain properties, or satisfy certain relations with each other. Furthermore, we may, at such a point, indicate the validity of these limitations. For this reason we will denote each area in which the validity of such limitations is being asserted, by a special box, which we call an assertion box.” (1947)
Herman Goldstine (1913 - 2004)
John von Neumann (1903 - 1957)
“How can one check a routine in the sense of making sure that it is right?
In order that the man who checks may not have too difficult a task the programmer should make a number of definite assertions which can be checked individually, and from which the correctness of the whole programme easily follows. ” (24 June 1949)
Alan Turing (1912 - 1954)
“ The basis of our approach is the notion of an interpretation of a program: that is, an association of a proposition with each connection in the flow of control through a program, where the proposition is asserted to hold whenever that connection is taken. ” (1967)
Robert Floyd (1936 - 2001)
“The intended function of a program, or part of a program, can be specified by making general assertions about the values which the relevant variables will take after execution of the program. These assertions will usually not ascribe particular values to each variable, but will rather specify certain general properties of the values and the relationships holding between them.” (October 1969)
Sir Tony Hoare (1934 - )
// x >= 0 and y = 0
y := 1;
// x >= 0 and y = 1
x := x+y;
// x >= 1 and y = 1
z := 3
// x >= 1 and y = 1 and z = 3
In this course, we will use Dafny, but we may discuss others.
Here's an example of contracts in Eiffel:
deposit (sum: INTEGER) is
-- Deposit sum into the account.
require
sum >= 0
do
add (sum)
ensure
balance = old balance + sum
end
Here's the same example in Dafny:
method deposit(sum: int)
modifies this
requires sum >= 0
ensures balance == old(balance) + sum
{
add(sum);
}
You have already discussed FOL in Lecture 3.
Here, $var$ is the name of a storage cell (variable) and $bexp$ is a quantifier-free first-order assertion.
// Oldest non-trivial algorithm known
// Assume M > 0 and N > 0
x := M; y := N;
while x != y do
if x<y then y := y-x
else x := x-y
// On termination: x == y
The command $\skipcmd$ does not change the state:
$$ \izero{Skip}{\ht{P}{\skipcmd}{P}} $$Consider the following triple $$ \ht{??}{x := x+1}{x=1} $$
Consider the following triple, where $E$ is an arbitrary expression and $Q$ is an assertion: $$ \ht{??}{x := E}{Q} $$
Substitution of a variable $x$ in $Q$ by $E$ is denoted by $$\subst{Q}{x}{E}$$
$$ \scriptsize \izero{Asgn}{\ht{\subst{(x=1)}{x}{1}}{x:=1}{x=1}} $$ which is the same as $$ \scriptsize \izero{Asgn}{\ht{1=1}{x:=1}{x=1}} $$
Note that $~~~ \scriptsize \izero{Asgn}{\ht{1=1}{x:=1}{x=1}} $
is different from $~~~ \scriptsize \izero{Asgn}{\ht{true}{x:=1}{x=1}} $
They are logically equivalent, but not syntactically equivalent!
Strengthening the precondition of a valid triple always produces another valid triple $$ \itwo{\textrm{Conseq Pre}}{\ht{P}{C}{Q}}{P\rightarrow P'}{\ht{P'}{C}{Q}} $$
Weakening the postcondition of a valid triple always produces another valid triple $$ \itwo{\textrm{Conseq Pos}}{\ht{P}{C}{Q}}{Q'\rightarrow Q}{\ht{P}{C}{Q'}} $$
Consider the triple $~~\ht{P}{C}{Q}$.
We can establish total correctness separately, since:
Total correctness = Partial correctness + Termination proof
The general approach for Hoare-style formal verification: