CSC148H Summer 1996   Assignment 2
----------------------------------

Specifications for the verify_table function:
---------------------------------------------

    % PRECONDITION
    assert (valid and
        number_of_trues (verify_plain) = 0 and
        number_of_trues (verify_cipher) = 0 and
        i = 1)
  
   % LOOP INVARIANT
   invariant (
         (valid = (number_of_trues (verify_plain) = i - 1
                   and number_of_trues (verify_cipher) = i - 1))
         and i >= 1 and i <= ALPHA_SIZE + 1 )

    % POSTCONDITION
    assert (valid = (number_of_trues (verify_plain) = ALPHA_SIZE
                     and number_of_trues (verify_cipher) = ALPHA_SIZE) )


The postcondition states that the table is valid if and only if the
number of trues in the verify_plain and verify_cipher arrays is equal
to ALPHA_SIZE.  In symbols, where N(x) is the # of trues in x,

   valid <==> N(verify_plain) = ALPHA_SIZE and N(verify_cipher) = ALPHA_SIZE

The precondition should be obvious.

The loop invariant comes from the postcondition.  At each iteration,
we should add one more true to each table, if the table is valid.  In
addition, for the proof to work out, we must ensure that i is in the
right range.  Here is the invariant I'll use in the proof

   valid <==> N(verify_plain) = i-1 and N(verify_cipher) = i-1
   and  1 <= i <= ALPHA_SIZE+1


Note: to shorten the proof, I will omit the parts for the
verify_plain array, but the reasoning is the same as for the
verify_cipher array.  I call the verify_cipher array 'cipher' in the
following.

----------------------------------------------------------------------------

1. Prove that the invariant is true at the beginning of every
   iteration.

   Proof:

   BASE CASE:  prove    valid <==> N(cipher) = i-1  and  1 <= i <= ALPHA_SIZE
       
       At the beginning of the first iteration, valid is true,
       i=1, and N(cipher) = 0 (from the precondition).  Therefore,
              valid <==> N(cipher) = 0   is true, so
	      valid <==> N(cipher) = i-1  is true also.

   IND HYP:  At the beginning of some arbitrary iteration assume the
       invariant is true.

   IND STEP: Prove it is true at the end of the iteration.

       Let i,i', valid,valid', cipher,cipher' be the values of the
       variables at the beginning and end of the iteration.

       CASE 1:  if  valid is false or i > ALPHA_SIZE,
           then the loop exits without having changed anything, so the
           invariant is still be true.

       CASE 2:  if  valid is true and i <= ALPHA_SIZE
           then the iteration proceeds.  At the end i is assigned i+1, so
               i' = i+1  (and i = i'-1).

           CASE 2A:  if  cipher(index_cipher) = true
               then valid is assigned false, and cipher is left unchanged, so 
                   valid' = false, and
                   cipher' = cipher
               Therefore N(cipher') = N(cipher) = i-1 = i'-2 not= i'-1
               That is, N(cipher') = i'-1  is false, but valid' is
               false also, so  valid <==> N(cipher) = i'-1  is true.
	       Also, since 1 <= i < ALPHA_SIZE, 1 <= i' <= ALPHA_SIZE+1, 
               Therefore, the invariant is true.

           CASE 2B:  if  cipher(index_cipher) = false
               then valid is left unchanged, so
                   valid' = true
               Now, cipher(index_cipher) is assigned true, so
                   cipher'(index_cipher) = true. 
               Therefore,  N(cipher') = N(cipher) + 1
                                      = i-1 + 1
                                      = i'-2 + 1
                                      = i'-1
               Since valid' = true,  valid' <==> N(cipher') = i'-1  is true,
               and 1 <= i' <= ALPHA_SIZE (from above argument),
               the invariant is true

       Therefore the invariant is true at the end of the iteration

    Therefore, by induction, it is true at the beginning (and end) of
    every iteration.

----------------------------------------------------------------------------

2. Partial Correctness 

    We know the invariant is true upon exit, but we have three cases
    on exit:

    CASE 1:  if valid is true and i > ALPHA_SIZE
        then from the invariant, i = ALPHA_SIZE + 1, and
            valid <==> N(cipher) = i-1  is true.  Therefore,
            valid <==> N(cipher) = ALPHA_SIZE is true also.

    CASE 2:  if valid is false and i > ALPHA_SIZE
        then from the invariant, i = ALPHA_SIZE + 1, and
            valid <==> N(cipher) = i-1  is true.  Therefore,
            valid <==> N(cipher) = ALPHA_SIZE is also true.

    CASE 3:  if valid is false and i <= ALPHA_SIZE
        then from the invariant 1 <= i <= ALPHA_SIZE, and
               N(cipher) not= i-1, so
               N(cipher) < i-1, so 
               N(cipher) not= ALPHA_SIZE.  Therefore,
            valid <==> N(cipher) = ALPHA_SIZE  is true.

     Therefore, the postcondition is true.
     Therefore, we have proved partial correctness.

----------------------------------------------------------------------------

3. Proof of Termination (by convergence method)

    First, by the invariant, 1 <= i <= ALPHA_SIZE+1; therefore,
        ALPHA_SIZE - i + 1 >= 0

    On each iteration, i is always incremented by 1; therefore,
        ALPHA_SIZE - i + 1 decreases by 1 on each iteration.

    So eventually, ALPHA_SIZE - i + 1 = 0, and then i = ALPHA_SIZE+1,
    which triggers the exit statement.

    Therefore the loop terminates.