# Introduction to Verification

## WHAT IS VERIFICATION?

Verification is demonstration that implementation "agrees" with a specification

### Specifiction:

• We have seen two forms of operational spec: FSM and Pnets
• Other forms of spec: DFD (operational), logic, algebra, functions (descriptive, denotational)
• Some are formal (mathematical definition of what syntax means), some are semi-formal or informal

## PROOF

• For formal specs, methods for demonstrating, via mathematical manipulation, transformation, and systematic reasoning, that the properties called for in a spec are present in some product.
• We might have formal specs for code modules, for design, for requirements... and then at each step in implementation we wish to verify "correctness". We show high-level design meets requirements specs We show set of module specs meets design specs
• The topic of the next few weeks: We wish to show that code for a module meets the module specs

## LOGIC as a Specification Notation

• predicte calculus is one form of descriptive specification
• use logic notation to describe relationships among values for program variables...
• Examples:
```     x < y and y < z

forall i ( a[i] >= b[i] )

d < 0  or  exists k ( d = k * m )

```

## PROGRAM STATES

• program state: a function (set of ordered pairs) mapping a value to each variable of interest
```     { (x,5), (y,"f77"), (z,-26.43), (pi,3.1415926) }
```
• A logic specification is a pattern that characterizes groups of program states.
```   { x < 5 }
```
is one specification, but it is satisfied by lots of program states:
```   { (x,3), (y, 1) (z,"abc") ... }
{ (x,3), (y, 1) (z,"def") ... }
{ (x,3), (y, 2) (z,"abc") ... }
{ (x,2), (y, 1) (z,"abc") ... }  etc...

```

## SPECS and PROGRAM EXECUTION

• Often we write specs that are concerned only with I/O vars...
```    IN  (for input, or initial state) and
OUT (for output, or final state)
```
• We want to know relationship between IN and OUT that is produced by execution of a program.
• notation:
```    { IN }  program  { OUT }
```
this says: "if the relationships expressed by 'IN' hold before execution of 'program' and if 'program' runs to completion (i.e. terminates properly), then the relationships expressed by 'OUT' will hold after execution.
• does not say 'program' will terminate...
• Alternate notation:
```    { PRE } program { POST }
```
Emphasizes the fact that the specs are preconditions and postconditions of execution.

## A GENERIC EXAMPLE: REASONING ABOUT PROGRAM STATES

Consider this algorithm and environment...
```   INITIAL STATE:
a can of beans, G and R
a pile of extra G beans (more than enough)

ALGORITHM:
while possible
draw out two beans
if both G or both R
return a G to the can
if one G and one R
put the R back in the can
end
```

## SEMI-FORMAL ARGUMENT

Questions:
• does this procedure terminate?
• if so, what is the relationship between the initial and final states?

There are two issues in program verification...

• partial correctness
• demonstrating a correspondence between implementation and specifications
• "if the program ends normally, then we know what properties must hold in the final state"
• termination
• must show that the program does end normally for input states in which the initial properties hold...

Together, these two are 'total correctness'

## SEMI-FORMAL REASONING

• Does the procedure terminate?

Yes.

Each loop interation removes two beans, but then places one bean back in the can.

Net change in bean count per iteration is -1.

Since the can starts with some non-negative bean count (a property of physical systems), and since the loop continues as long as two beans remain in the can, the lower limit of 0 or 1 bean in the can must be reached eventually no matter how many beans are initially there.

• What is the relationship of IN to OUT? Need to produce specs in logical notation

An invariant: a property that hold at some point in computation no matter how many times that point is reached.

Loop invariant: an invariant chosen to hold at the beginning of each execution of a loop body.

• Invariant INV:
```   #R mod 2 stays the same.
```
• Proof

consider the effect of each iteration on the proposed 'invariant' property...

assume INV holds before loop body is executed.

```    if get 2 R, then #R becomes #R-2, INV holds
if get 2 G, no change in #R so INV holds
if get 1 G 1 R, no change in #R so INV holds
```

So, if INV holds before loop, it also holds after.

The program consists of just this one loop.

Thus the relationship of IN to OUT is:

```    if start with even #R, end with even #R
```

Stated in predicate calculus:

```   { IN:  r0 = #R }
while possible
draw out two beans
if both G or both R
return a G to the can
if one G and one R
put the R back in the can
end
{ OUT: (r0 mod 2) = (#R mod 2) }
```

## INFERENCE SYSTEMS

• inference system:
• axioms
• rules of inference
• proof:
• sequence of formulae
• each formula is either an axiom, or can be derived from axioms and previous formulae by aplication of rules of inference
• f1, f2, f3, ... , fn is a proof of |- fn if for each i:
```   axiom(fi), or |- fi using f1, ... , f(i-1)
```
• Example: inference rule
```    All men are mortal     |
Socrates is a man      |
--------------------   +--- Modus Ponens
Socrates is mortal     |
```
The famous syllogism is an example of application of a rule of inference in an inference system
• Example: integer arithmetic
```   axioms
x + y = y + x
x * y = y * x
x * (y + z) = (x * y) + (x * z)
x + 0 = x
x * 0 = 0
x * 1 = x   etc...

rules of inference
( a = b )  ==>  ( c * a = c * b )
( a < b ) and ( c < 0 )  ==>  ( c * a > c * b )
```

## HOARE'S AXIOMATIC METHOD

We will see in the notes on the Axiomatic Method of program verification will use an extended inference system:
• axioms of arithmetic, etc...
• new axioms for assignment statements
• inference rules for each control structure
• other supporting inference rules