x>3 & y>5

* in a program:

- always possible as comments

- some languages provide

ASSERT

 ASSERT y > 5; x := y - 2; ASSERT x > 3 & y > 5; 

* can «chain» assertions

{ F₁ }

S1

S2

Program with assertions are manipulated in a formal deduction system based on proof rules, such as

S1 {F2} ,
   {F2} 
S2 {F3}
                                   

______________________________________________________________________________________________________________________________________
{F1} 
S1 ; 
S2
{F3}

These proof rules are in the same spirit as the proof rules of
«classical» logic, such as 
                               A ,  A => B
                                   

                               ___________
B




                   Assertions and Loops


Loop Invariant:

an assertion preserved by the body of a loop

If {F} is invariant for a particular loop (body)

then {F} is preserved by the entire loop

proof: by induction on number of iterations

Write {{F}} to indicate F is a loop invariant




                   Example Procedure


 
 Procedure
   BubbleSort(
   A:  
 ARRAY OF INT
 , lim:  
 INT
  );
    
 for
  i := 2  
 to
  lim  
 do
 
      j := i;
       
 while
  j>1  
 and
  A[j] 
 do
 
         A[j] :=: A[j-1];
         j := j-1
       
 end
 
    
 endfor
 ;



******     OMITTED OVERLAY      ******



                   Procedure Pre- & Post-conditions


{  
 lim, A[1..lim] are integers
   }
 
 Procedure
   BubbleSort(
   A:  
 ARRAY OF INT
 , lim:  
 INT
  );


   i := 2;
    
 while
  i<=lim  
 do
 
      j := i;
       
 while
  j>1  
 and
  A[j] 
 do
 
         A[j] :=: A[j-1];
         j := j-1
       
 end
 
      i := i+1;
    
 end
 ;
{  
 values in A unchanged &
  
   
 lim, A[1..lim] are integers &
  
   
 i = lim +1 &
  
   
 forall x, 1   }

Also, the   
 for
   loop rewritten
into simpler components




                   Loop Invariants


 
 Procedure
   BubbleSort(
   A:  
 ARRAY OF INT
 , lim:  
 INT
  );
   i := 2;
    
 while
  i<=lim  
 do
 
      { 
  A[1..i-1] sorted
   }
      j := i;
       
 while
  j>1  
 and
  A[j] 
 do
 
         A[j] :=: A[j-1];
         j := j-1
       
 end
 
      { 
  A[1..i] sorted
   }
      i := i+1;
      { 
  A[1..i-1] sorted
   }
    
 end
 ;
{  
 i = lim+1 &
  
   
 A[1..lim] sorted
   }


Note - certain less important assertions omitted





                   Loop Invariants


 
 Procedure
   BubbleSort(
   A:  
 ARRAY OF INT
 , lim:  
 INT
  );
   i := 2; { 
 A[1] sorted
  }
   {{ 
  A[1..i-1] sorted
   }}
    
 while
  i<=lim  
 do
 

      j := i;
      {{ 
  A[1..j-1] sorted &
         A[j..i] sorted     
  }}
       
 while
  j>1  
 and
  A[j] 
 do
 
         A[j] :=: A[j-1];


         j := j-1
       
 end
 
      { 
  A[1..i] sorted
   }
      i := i+1;

    
 end
 ;
{  
 i = lim+1 &
  
   
 A[1..lim] sorted
   }





                   Loop Invariant Formalism


Let  
 I
   (intended  as  the loop  invariant) and


 
 cond
  
(where  
 ~
  
 cond
   is intended as the loop termination condition)
be  assertions.

The formal inference rule for a loop with a body  
 B
   is:

{  
 I & cond
   }  
 B
   {  
 I
   }
                                   

________________________________________________________________________________________________________________________________________________________________________________________________
{ 
 I
  }  
 while 
  cond  
 do 
  B  
 end
   { 
 I &  
 ~ 
 cond
 }

Invariant assertions only worthwhile if loop terminates





                   Termination


          
{   
 x > y 
  }
          
{{  
 x > y 
  }}
           
 while 
  x <> 0  
 do
  
                  x := x-2 ;
                  y := y-2 ;
           
 end
 
          {  
 x > y & x = 0 
  }


The proof rule shows the above to be correct

but the loop terminates

if and only if  
 x
   is initially even
and positive.




                   Loop Invariants and Induction


Tail recursion => iteration
   
 f( i, x ) := if ( i=0 )
     then g(x)


     else h( i, f( i-1, x ) ) 
  

becomes
   
 f( m, x ) {
     r := g(x);
     for i = m until 1 do
         r := h( i, r );
     return r }
  

Loop invariant on iterative version is
very close to induction on recursive version




                   Loop Invariants as Design Aid


Formalism is
not
necessary

Ask:

* What is changed in this loop?

* What is preserved in this loop?

Look for higher-level concepts/properties


(such as part of array being sorted)





                   Back to Termination


It would be valuable to have a method to discover
whether or not a program terminates.

Why not just run it?

* Fundamental limitation to computer science




                   The Halting Problem


(A problem is a set of inputs which we would like
to classify by some program.)

Q: Can we tell whether or not an arbitrary program halts?

A: In general, no!

Intuition for the proof:

                This statement is false.



                       true    =>    false

                      false    =>    true

This contradiction requires:
     +o         self-reference
     +o         negation




                   Statement & Proof Outline


Theorem:
It is impossible to write a procedure
that decides whether an arbitrary program halts.

Outline:
proof by contradiction

1. assume the result is false
(i.e. such a procedure
does
exist)

2. define a new program using assumption

3. consider cases when this new program halts
a.     if it halts => it doesn't
b.     if it doesn't => it does

hence program cannot be constructed, so procedure does not
exist.




                   Proof - Step 1


Assume there is a Boolean procedure 
DoesHalt?
 such that:


DoesHalt?
(Pfile) returns

       true
       if the program represented by Pfile halts
       and

       false
       if the program goes into an infinite loop.

Preconditions:

       a. Pfile is a text file

       b. Pfile represents a syntactically correct program

Postconditions:



       a. Pfile is not changed

       b. The value
       true
       or
       false
       is returned as indicated above




                   Proof - Step 2


On the file Confound put the program:

/* file  Confound */
main( )

#include DoesHalt?

{
   if (DoesHalt?( __________ ))
   {    /* loop forever */
        while ( true ) { };
   }
}

(will fill in "
__________
" later)


That is, the program 
Confound halts
       if   
DoesHalt?
(__________)
       is   FALSE

but it loops forever
       if   
DoesHalt?
(__________)
       is   TRUE.





                   A «Thought Experiment»


Pretend to execute the program by:

1. compiling the program file 
Confound

2. running the compiled program

That is:

%cc Confound

%a.out


  
What would happen???



  
Would it halt???




                   Proof - Step 3


Two cases: 
DoesHalt?
 in 
Confound

o either returns
TRUE

o or it returns
FALSE:

case 1 -

DoesHalt?("Confound")
             is TRUE
                                    =>
the program loops
                                    =>
DoesHalt?("Confound")
             is FALSE

case 2 -

DoesHalt?("Confound")
             is FALSE
                                    =>
the program halts
                                    =>
DoesHalt?("Confound")
             is TRUE




                   Consequences of Halting Problem


* halting problem takes on many «disguises»

* virtually any program that takes other programs as
input is vulnerable:

       * compiler optimization
       

       dead code elimination

       * program verification
       


       * concurrency synchronization

       * expert systems

* sometimes restrict power to avoid trap

       * SQL, other database query
              languages

* in general, a valuable warning


                              n 
IF
's, 2n possible paths




                   Testing and Formal Verification

                           exhaustive testing impossible
Rall the complexity problem with testing a long chain
oPfro<vPiRnEg>ItFh<a/tPRmEa>n'ys:conditions are mutually exclusive
<>
<=A> HmRaEnFy="fIemwaegresp/oqsasIiIb-liemgp-a0t.hpsdf">
<<PI>MG src="Images/qaII-img-0.jpg" width="240" alt="">
e=x>paenxdhatuhsitsivfeigtuerset<s/Am>ay be possible




                   Proofs in Practice


* dependence on formal specifications
                              =>


cannot prove systems with complex interactions

* program proving useful for critical internal modules

       - abstract data types (ADT's)

       - synchronizations

* proofs complement testing


useful for hard-to-test situations




                   Proofs in Practice


Just as the typical mathematician does not
prove theorems using the predicate calculus,
the typical computer scientist should not
prove programs by formal deduction.

Hence

* human-readable proofs

* «programmer's assistant» to handle details

* CASE tools should facilitate use of assertions

Proof-like algorithms often internal
*      type checking
*      database validation




                   Example: Trusted Agents



Goal:
admit «foreign» code inside of «firewall»

Application: network protocol checkers


small, quick

Traditional approaches: interpretation,   bounds checking


essentially, a mini-firewall

Alternative:
foreign module
includes
both code &
proof
of proper behavior

       * use the fact that proof
       checking
       is easy even if proof
       discovery
       is hard




                   Ten Commandments of Formal Methods


1. choose appropriate notation

2. formalize but don't over-formalize

3. estimate costs

4. have a formal methods expert on call

5. augment rather than replace traditional methods

6. document sufficiently

7. don't compromise other quality standards

8. do not be dogmatic

9. test, test, and test again

10. reuse
 -  after Bowan and Hinchley, Computer April 1995 


Additional Reading:

R. A. DeMillo, R. J. Lipton, & A. J. Perlis, "Social Processes
and Proofs of Theorems and Programs,"  Comm. ACM 22,5 (May 1979),
271-280.  responses Comm. ACM 22,11 (Nov. 1979) 621-630.

D. L. Parnas, "Software Aspects of Strategic Defense Systems,"
Comm. ACM 28,12 (Dec. 1985), 1326-1335.  responses Comm. ACM
29,7 (July 1986), 591-592; 29,9 (Sept 1986), 830-831.



 © Copyright Edward Robertson, 2109-2-16