Verification is demonstration that implementation "agrees" with a specification
x < y and y < z forall i ( a[i] >= b[i] ) d < 0 or exists k ( d = k * m )
{ (x,5), (y,"f77"), (z,-26.43), (pi,3.1415926) }
{ 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...
IN (for input, or initial state) and OUT (for output, or final state)
{ 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.
{ PRE } program { POST }Emphasizes the fact that the specs are preconditions and postconditions of execution.
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 discard both return a G to the can if one G and one R put the R back in the can end
There are two issues in program verification...
Together, these two are 'total correctness'
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.
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.
#R mod 2 stays the same.
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 if start with odd #R, end with odd #R
Stated in predicate calculus:
{ IN: r0 = #R } while possible draw out two beans if both G or both R discard both 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) }
axiom(fi), or |- fi using f1, ... , f(i-1)
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
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 )