Assertion Based Verification

“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)

Assertion Based Verification

“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)

Assertion Based Verification

“ 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)

Assertion Based Verification

“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 - )

Hoare Logic

• Hoare Logic originated in the 1960s, but it continues to be the subject of intensive research right up to the present day.
• It lies at the core of a multitude of tools that are being used in academia and industry to specify and verify real software systems.

Hoare Logic

• Hoare Logic combines two beautiful ideas:
  • a natural way of writing down specifications of programs
  • a compositional proof technique for proving that programs are correct with respect to such specifications

Sir Tony Hoare

• Sir Tony Hoare has made many important contributions to Computer science. Perhaps his most well-known invention is the Quicksort algorithm, but Hoare Logic and the language CSP were extremely influential in the programming language community.

Alexandra Mendes, Sir Tony Hoare, and João F. Ferreira. Symposium on Formal Methods. October 2019

• He received many prizes including the ACM Turing Award (1980) and the IEEE John von Neumann Medal (2011)
• He is currently 86 years old, but still active!

States and Assertions

• Executing an imperative program has the effect of changing the program state, i.e. the values of program variables.
• Sets of states can be characterized by assertions.
• We can use assertions to express properties that hold at particular points during a program's execution: they are claims about the current state of the program when execution reaches that point.

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

Which of the following Hoare triples are valid?

1. $\ht{x=2}{x := x+1}{x=3}$ Valid!
2. $\ht{x \neq 0}{y := x*x}{y > 0}$ Valid!
3. $\ht{x \ge 0}{y := 2*x}{y > x}$ Invalid!
4. $\ht{true}{\ifthenelsecode{x>7}{y:=1}{y:= 3}}{y < 4}$ Valid!

Design by Contract (DbC)

• Design By Contract (DbC) is a software correctness methodology
• Term coined by Bertrand Meyer; central concept in the Eiffel programming language
• A contract can be summarised by the "three questions" that the designer must repeatedly answer in the contract:
  • What does the contract expect?
  • What does the contract guarantee?
  • What does the contract maintain?

Design by Contract (DbC)

• Contracts allow:
  • To record details of methods’ responsibilities and assumptions
  • To document the intended behaviour (specification) of software components
  • To avoid having to repeatedly check arguments
  • To assign blame across interfaces

Design by Contract (DbC)

• Contracts are:
  • More abstract than code (e.g., sqrt() might be implemented using linear search, Newton’s method, . . .)
  • Not necessarily checkable (e.g., quantified over infinite types, or just textual strings)
    • In cases where they are formalized, it is usually possible to automatically generate verification conditions
  • (Or can be) used to avoid performing time-consuming defensive checks inside production code

Design by Contract (DbC)

• Modularity of Reasoning
  • As far as verification is concerned: a program is fully verified if each annotated component is individually verified
  • In order to understand what the code does, one can read the contracts instead of looking at all the code
• Other features
  • Designs and implementations can be refined by refining contracts
  • DBC can be used to understand, document, improve, and maintain an existing code base
  • DBC can be used to generate tests and to formally verify key subsystems

Design by Contract (DbC)

• Language support for contracts exists in different forms:
  • Natively: Eiffel, Racket, SPARK Ada, Dafny, ...
  • Third-party: JML for Java; Spec# for C#; PyContracts for Python; ...

In this course, we will use Dafny, but we will discuss others.

Design by Contract (DbC)

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

Design by Contract (DbC)

Here's the same example in Dafny:

method deposit(sum: int)
modifies this
requires sum >= 0
ensures balance == old(balance) + sum
{
    add(sum);
}

Design by Contract (DbC)

Here's an example of contracts in Java (OpenJML):

public class Subtract {
    //@ requires a > 0;
    //@ requires b > 0;
    //@ ensures \result == a-b;
    public static int subtract(int a, int b){
        return a-b;
    }

    public static void main(String args[]){
        System.out.println(subtract(2,3));
    }
}

Formal Reasoning with Hoare Logic

Assertions

• We need a language that enables unambiguous specifications: we will use FOL to express assertions

A simple programming language

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

Hoare Logic

• Hoare Logic provides axioms and inference rules for all the constructs of a programming language
• Inference rules are of the form $$\ithree{\textrm{rule name}}{\textrm{Conclusion}}{\textrm{Premise 1}}{\cdots}{\textrm{Premise n}}$$
• Rules without premises are called axioms

Axiom for skip

The command $\skipcmd$ does not change the state:

Assignment

Consider the following triple $$ \ht{??}{x := x+1}{x=1} $$

• What precondition can we use?
• How can we obtain a precondition from the assignment and postcondition?
  • The value of $x$ after executing the assignment should equal the value of $x+1$ in the state before executing it.
  • We can replace ?? with $x=0$

Assignment

Consider the following triple, where $E$ is an arbitrary expression and $Q$ is an assertion: $$ \ht{??}{x := E}{Q} $$

• How can we obtain a precondition from the assignment and postcondition?
  • The value of $x$ after executing the assignment should equal the value of $E$ in the state before executing it.
  • For $Q$ to be true after the assignment, the assertion obtained by substituting $E$ for $x$ in $Q$ must be true before executing it.

Substitution

Substitution of a variable $x$ in $Q$ by $E$ is denoted by $$\subst{Q}{x}{E}$$

• $\subst{Q}{x}{E}$ is the assertion obtained by replacing all free occurrences of $x$ in $Q$ by $E$
• Examples:
  • $\subst{(x=1)}{x}{x+1} = (x+1=1)$
  • $\subst{(x\leq y)}{x}{x+1} = (x+1\leq y)$

Axiom for assignment

Example

$$ \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}} $$

Consequence Rules

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!

Consequence Rules

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}} $$

Consequence Rules

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'}} $$

Example: our first proof

• Putting the rules we've seen together, we can prove $$ \scriptsize {\ht{x=0}{x := x+1}{x\ge 1}} $$
• The proof is a derivation tree: $$ \scriptsize \itwo{\textrm{Conseq Pre}}{\ht{x=0}{x := x+1}{x\ge 1}} {\icond{x=0 \rightarrow x+1\ge 1}} {\izero{\textrm{Asgn}}{\ht{x+1\ge 1}{x := x+1}{x\ge 1}}} $$

Prove that the following triples are valid

1. $\ht{true}{x := 42}{x\ge 10}$
2. $\ht{x=2}{x := x+1}{x=3}$
3. $\ht{x \neq 0}{y := x*x}{y > 0}$

Rule for Sequential Composition

• In words: if $C1$ transforms any state that satisfies $P$ into any state that satisfies $Q$, and if $C2$ transforms a state that satisfies $Q$ into any state that satisfies $R$, then $C1;C2$ transforms any state that satisfies $P$ into a state that satisfies $R$.

Example

• Show that $~~~ \scriptsize \ht{x=0}{y:=2\,;\,x:=y+1}{x=3} $
• Derivation tree:
  $ \tiny \itwo{\textrm{Seq}} {\ht{x=0}{y:=2 ; x:=y+1}{x=3}} {\itwo{\textrm{Asgn}}{\ht{x=0}{y:=2}{y+1=3}} {\icond{x=0\,\rightarrow\,2+1=3}} {\izero{\textrm{Asgn}}{\ht{2+1 = 3}{y := 2}{y+1 = 3}}}} {\izero{\textrm{Asgn}}{\ht{y+1=3}{x:=y+1}{x=3}}} $

Prove that the following triples are valid

1. $\ht{x=0}{x := x+1; x := x+2}{x=3}$
2. $\ht{x=0}{x := x+1; \skipcmd}{x=1}$
3. $\ht{x=2 \wedge y=3}{x :=x+2; y := y+1}{x=y}$

Rule for Conditionals

• In words: if $b$ is true, the first branch is executed and we need to establish $\ht{P}{C1}{Q}$; otherwise, the second branch is executed and we need to establish $\ht{P}{C2}{Q}$

Rule for While Loops

• When the loop terminates, we know that $b$ is false
• The assertion $P$ is called an invariant

Prove that the following triple is valid

1. $\ht{x\ge 0}{\whileloop{x>0}{x:=x-1}}{x=0}$

Summary

Partial vs. Total Correctness

Consider the triple $~~\ht{P}{C}{Q}$.

• Partial correctness: if command $C$ is started in a state satisfying assertion $P$, and if $C$ terminates in some final state, then this final state will satisfy the assertion $Q$.
• Total correctness: if command $C$ is started in a state satisfying assertion $P$, then it terminates and it does so in a final state that satisfies the assertion $Q$.

Soundness

• Soundness: only valid Hoare Triples can be proved by the rules.
• To demonstrate soundness, we can use induction over the derivation trees. We have to show that:
  • The Hoare triples in the axioms are correct
  • For each inference rule, assuming that the triples in the premises are valid, we show that the triple in the conclusion is also valid.
• Soundness is proved w.r.t. the semantics of the programming language.

Completeness

• Completeness: all valid Hoare Triples can be proved by the rules.
• Completeness is relative to the logic language used.
  • For example, invariants and assertions have to be expressible in the logic.
• Soundness is proved w.r.t. the semantics of the programming language.

Hoare Logic in verification tools

General approach for Hoare-style formal verification:

1. A programmer annotates the source code
2. A tool analyses the code and attempts to show that all the assertions given can be derived using the rules of Hoare Logic
3. The tool may be able to do this unassisted
4. If not, it emits verification conditions, purely logical assertions that need to be checked
5. These may be passed on to an automated theorem prover, or some other decision procedure
6. In extreme cases verification conditions may not be solved automatically and require interactive theorem proving by an expert or the provision of extra hints