Printable Version of this PageHome PageRecent ChangesSearchSign In

[Apr 07]

html xmlns:o="urn:schemas-microsoft-com:office:office"
xmlns:w="urn:schemas-microsoft-com:office:word"
xmlns="http://www.w3.org/TR/REC-html40">







Infering Loop Invariant








A program state can be expressed as a logical formula.



If P is the path condition and V denote the assignment of
symbolic values v1, v2,Tt(Bo program variables x1, x2.. then the state can be
expressed as a logical formula



P span
style='font-family:Symbol;mso-ascii-font-family:"Times New Roman";mso-hansi-font-family:
"Times New Roman";mso-char-type:symbol;mso-symbol-font-family:Symbol'>span
style='mso-char-type:symbol;mso-symbol-font-family:Symbol'> (v1

 x1) span style='font-family:Symbol;mso-ascii-font-family:"Times New Roman";
mso-hansi-font-family:"Times New Roman";mso-char-type:symbol;mso-symbol-font-family:
Symbol'>
(v2 = x2 ) span style='font-family:Symbol;mso-ascii-font-family:"Times New Roman";
mso-hansi-font-family:"Times New Roman";mso-char-type:symbol;mso-symbol-font-family:
Symbol'>
,T<(B/p>

 



Given a loop invariant, properties about loops can be
verified as follows:



while( b ){



//
loop_invariant I



B;



}



assert P;



 



Proof Obligation: span style='font-family:Symbol;
mso-ascii-font-family:"Times New Roman";mso-hansi-font-family:"Times New Roman";
mso-char-type:symbol;mso-symbol-font-family:Symbol'>span style='mso-char-type:
symbol;mso-symbol-font-family:Symbol'>b span style='font-family:
Symbol;mso-ascii-font-family:"Times New Roman";mso-hansi-font-family:"Times New Roman";
mso-char-type:symbol;mso-symbol-font-family:Symbol'>span style='mso-char-type:
symbol;mso-symbol-font-family:Symbol'> I span style='font-family:
Symbol;mso-ascii-font-family:"Times New Roman";mso-hansi-font-family:"Times New Roman";
mso-char-type:symbol;mso-symbol-font-family:Symbol'>span style='mso-char-type:
symbol;mso-symbol-font-family:Symbol'> P



 



A logical formula I is a loop invariant, if




  1. I
    holds before entering the loop

  2. If we
    execute loop body B starting from
    a state satisfying I, the final state also satisfies I.



 



Union of all reachable states is a loop invariant.



Let S0 be the program state before the loop is
entered. And S1, S2 ,Tb(Be the program states that after B
is executed 1, 2,,T (Bnumber of times. Then a loop invariant is S0 span
style='font-family:Symbol;mso-ascii-font-family:"Times New Roman";mso-hansi-font-family:
"Times New Roman";mso-char-type:symbol;mso-symbol-font-family:Symbol'>span
style='mso-char-type:symbol;mso-symbol-font-family:Symbol'> S1
span style='font-family:Symbol;mso-ascii-font-family:"Times New Roman";
mso-hansi-font-family:"Times New Roman";mso-char-type:symbol;mso-symbol-font-family:
Symbol'>
,T<(B/p>

A nave algorithm to compute a loop invariant symbolically
executes the loop body iteratively until a fixed point is reached. But no
guarantee of termination!



 



Cormac Flanagan$(Bs (Bsolution (PoPL 02):



I = abstract( S0 )



while( true )



Q =
postcondition( B, I ) //returns
the logical formula corresponding to the program state after executing B
assuming I holds initially



next = I span
style='font-family:Symbol;mso-ascii-font-family:"Times New Roman";mso-hansi-font-family:
"Times New Roman";mso-char-type:symbol;mso-symbol-font-family:Symbol'>span
style='mso-char-type:symbol;mso-symbol-font-family:Symbol'>
abstract( Q )



if( next ==
I ) then I is the loop invariant. So Stop.



I = next



end while



 



Drawback:




  1. Requires
    a set of predicates to be specified

  2. Failure
    to prove the property does not necessarily mean the program is buggy. It
    is may be that set of predicates isn$(Bt (Badequate.



 



 







Last modified 7 April 2005 at 12:56 am by Saswat Anand