Verification Conditions

Let us consider the bubble sort example. Using the SP, an annotated version is obtained as follows:

{ Inv_l: Vi e INDEX-x, ASX_INDEX-1J , t(i) = nth-highest (t, i) }

i Vie !MAX_INDEX-xr!4AX_INDEX-l]r t (i) = nth-highest (t, i) a y=0 } { Inv_2: Vie [¡■&X_INDEX-x,!'!AX_INDEX-l], t (i) = nth-highest It,i)

(Vie[liPiX_IWEX-x,!tAX_I!'lDEX-llr t Ci) = nth -highest (t, ij

( Vie iMAX_INLiEX-xrMAX_INDEX-ll, t (i) = nth-highest (t, i!

( Vi £ [MAX_INDEX-xtMAX_IfiIDEX-11, t fij = nth-highest it,i| A t (y) = œx(t ' [0,y] )

f Vi e [MAX_INDEX-x, MAX_IfilDEX-1], t (i) = nth-hlghest (t,i) A t (y) = maxlt '[Ory]) A tmg = t ' (y+l)

A t =t'++[y+l -> t ' (y) ] ++ (y -> t'(y+l)]> }

(Vie iMAX_INDEX-x,MAX_INDEX-l I, t (i ) = n th-highest (t,i) A t (y) = max ft ' f 0, y] ) ) A £J3P = t ' (y+l)

(Vie (MAX_ INDEX-x, MAX_INDEX-1 ], t (i) - nth-highest (t, i) A t(y) = max (t ' 10, y])) }

loop_vc_inv2:

! Vie [MAX_INDEX-x,MAX_INDEX-l], t (i) = nth-highest (t, ii A t(y) = nmx(t ' iO,yl)

A Vi e [¡<iAX_INDEX-x,MAX_INDEX-l], t (i) = nth-highest (t, i) A t (MJiX_INDEX-x-l) = maxft' [0,MAX_INDEX-x-l ] } }

LOCSLVCLINV! :

A Vie iMAX_INDEX-x+l, MAX_INDEX-1], t (i ) = nth-highest ft, i) ^ t (y) = mzxff [0,yl ) => Inv_l }

ByfeblesortJVC :

A Vie [I4AX_INDEX-x,!&LX_INDEX-1 ], t (i) = nth-highest (t, i) => Post-bubbieso^t |/

[Post-btàblesort : Vie [0,MAX_INDEX-1 ] r t(i> <=t {i+l>> } }

In this function, a state predicate is inserted (in italics and between curly brackets) at every location in the code. These predicates have been computed from top to bottom, using SP: The precondition, the invariants, and the post-conditions were positioned beforehand and then the other predicates were computed. Verification conditions have been obtained: LOOP_VC_INV1 and LOOP_VC_lNV2 are associated to the two loops, respectively, and placed at their bottom. Their LOOP_VC_PRE and LOOP_VC_POST are not given here as they are trivial. Bubblesort_VC represents the verification condition associated with the whole function as it is equal to SP(f,pre_f) =>post_f. We invite the reader to prove the truth of the verification conditions. Notice that the symbol ++ denotes functions overriding: f ++ [x ->e] overrides f at point x. The result is the function, let g, defined by g = lambda y. if y=x then e else f(x)

Proofs of VC can be done by hand or using some specialized tool such as a theorem prover. Such tools are highly specialized and some deductive provers (such as the Prototype Verification System (PVS); see http://www.csl.sri.com/programs/formalmethods/) can reason quite similarly to humans.

Was this article helpful?

0 0
The Ultimate Computer Repair Guide

The Ultimate Computer Repair Guide

Read how to maintain and repair any desktop and laptop computer. This Ebook has articles with photos and videos that show detailed step by step pc repair and maintenance procedures. There are many links to online videos that explain how you can build, maintain, speed up, clean, and repair your computer yourself. Put the money that you were going to pay the PC Tech in your own pocket.

Get My Free Ebook


Post a comment