CSE 438/538.ASSIGNMENTS

The following four assignments illustrate the most important verification activities of already developed software, in a “recommended” order of application.

1. Static Analysis in Quality Assurance should be carried out first to detect real or potential problems with the software without its execution.

2. Program Testing, which includes the requirements-based Black-Box testing and code-based Structural Testing should be used next. It should also be noted here that Static Analysis is a prerequisite to structural testing, i.e. the latter cannot be carried out without some sort of the former.

3. Dependency Analysis is usually used to help in reasoning about the program, either during its debugging or modifications.

4. Formal Proof which, if successful, is the only absolute evidence of program correctness, is usually applied only to the most critical and relatively small part of the code.

That kind of analysis is usually of proscritpive nature. 
That is, it identifies potential or real problems with the code, e.g.
the use of uninitialized variables.  

Consider the following listing of the SPARK Examiner’s 
analysis of the package TestResults, which contains five 
procedures and one function.

     *******************************************************
                           Listing of SPARK Text
       SPARK95 Examiner with VC and RTC Generator Release 2.5 / 04.97
                           Demonstration Version
          *******************************************************


                       DATE : 02-NOV-1999 13:27:03.72

Line
   1  package TestResults
   2  is
   3      pragma Elaborate_Body(TestResults);
   4  end TestResults;
   5  
   6  package body TestResults
   7  is
   8  
   9  type Alert is (Warning, Caution, Advisory);
  10  
  11    procedure ExtGCD1(M, N    : in  POSITIVE;
  12                      X, Y, Z : out INTEGER)
  13    --  procedure is error-free;
  14    --# derives X from M, N &
  15    --#         Y from M, N &
  16    --#         Z from M, N;
  17    is
   18      A1, A2, B1, B2, C, D, Q, R, T : INTEGER;
  19    begin
  20      A1 := 0; A2 := 1; B1 := 1; B2 := 0;
  21      C := M; D := N;
  22      while D /= 0 loop
  23        Q := C/D; R := C - Q * D;
  24        C := D; D := R;
  25        A2 := A2 - Q * A1; B2 := B2 - Q * B1;
  26        T := A1; A1 := A2; A2 := T;
  27        T := B1; B1 := B2; B2 := T;
  28      end loop;
  29      X := C; Y := A2; Z := B2;
  30    end ExtGCD1;

+++        Flow analysis of subprogram ExtGCD1 performed: 
           no errors found.

  31  
  32    procedure ExtGCD2(M, N    : in  POSITIVE;
  33                      X, Y, Z : out INTEGER)
  34    
  35    --# derives X from M, N &
  36    --#         Y from M, N &
  37    --#         Z from M, N, X;
								 ^1

  38    is
  39      A1, A2, B1, B2, C, D, Q, R, T : INTEGER;
  40    begin
  41      A1 := 0; A2 := 1; B1 := 1; B2 := 0;
  42      C  := M; D  := N;
  43      while D /= 0 loop
  44        Q := C/D; R := C - Q * D;
  45        C := D; D := R;
  46        A2 := A2 - Q * A1; B2 := B2 - Q * B1;
  47        T := A1; A1 := A2; A2 := T;
  48        T := B1; B1 := B2; B2 := T;
  49      end loop;
  50      X := C; Y := A2; Z := B2;
  51    end ExtGCD2;
  52  
  53    procedure ExtGCD3(M, N    : in  POSITIVE;
  54                      X, Y, Z : out INTEGER)
  55    
  56    --# derives X from M, N &
   57    --#         Y from M, N &
  58    --#         Z from M, N;
  59   
  60   is
  61      A1, A2, B1, B2, C, D, Q, R, T : INTEGER;
  62   begin   
  63      A1 := 0;
  64      if A1>0 then A1 := 2; else A2:=2; end if;
                  ^2

                  
  65      B1 := 1; B2 := 0;
  66      C := M; D := N;
  67      while D /= 0 loop
  68        Q := C/D; R := C - Q * D;
  69        C := D; D := R;
  70        A2 := A2 - Q * A1; B2 := B2 - Q * B1;
                  ^3

                          
  71        T := A1; A1 := A2; A2 := T;
  72        T := B1; B1 := B2; B2 := T;
  73      end loop;
  74      X := C; Y := A2; Z := B2;
                                 ^4

  75    end ExtGCD3;

       
  76  
  77    procedure ExtGCD4(M, N    : in  POSITIVE;
  78                      X, Y, Z : out INTEGER)
  79    
  80    --# derives X from M, N &
  81    --#         Y from M, N &
  82    --#         Z from M, N;
  83    is
  84      A1, A2, B1, B2, C, D, Q, R, T : INTEGER;
  85    begin
  86      A1 := 0; A2 := 1; B1 := 1; B2 := 0;
                                          ^6

  
   87      C := M; D := N;
  88      while D /= 0 loop
  89        Q := C/D; R := C - Q * D;
  90        C := D; D := R;
  91        A2 := A2 - Q * A1; B2 := B2 - Q * B1;
                                               ^7

  92        T := A1; A1 := A2; A2 := T;
  93        T := A1; B1 := B2; B2 := T;
                              ^8

  94      end loop;
  95      X := C; Y := A2; Z := B2;
  96    end ExtGCD4;
  97  
  98    procedure ExtGCD5(M, N    : in  POSITIVE;
  99                      X, Y, Z : out INTEGER)
 100   
 101    --# derives X from M, N &
 102    --#         Y from M    &
 103    --#         Z from M, N;
 104    is
 105      A1, A2, B1, B2, C, D, Q, R, T : INTEGER;
 106    begin
 107      A1 := 0; A2 := 1; B1 := 1; B2 := 0;
 108      C := M; D := N;
 109      while D /= 0 loop
 110        Q := C/D; R := C - Q * D;
 111        C := D; D := R;
 112        A2 := A2 - Q * A1; B2 := B2 - Q * B1;
 113        T := A1; A1 := A2; A2 := T;
 114        T := B1; B1 := B2; B2 := T;
 115      end loop;
 116      X := C; Y := A2; Z := B2;
 117    end ExtGCD5;

 
 118  
 119  function RingBell(Event: Alert) return Boolean 
 120  
 121  is
 122  
 123  Result: Boolean;
 124  
 125  begin
 126  
 127  if Event = Warning
 128  then Result := true;
 129  elsif Event = Advisory then
 130  Result := false;
 131  end if;
 132  
 133  return Result;
                     ^10

                      
 134  end RingBell;

 135  
 136  end TestResults;

1. Error # 1
   1. X cannot be imported, declared OUT
   2. N/A
   3. N/A
2. Error # 2
   1. Whenever 64 is reached, A1 has always the same value.
   2. There is 0 M A1 for 63, and there is no other expression e,
      for which e M A1. Since 64 is always done after 63, the value
      of A1 on entry to 64 depends on a constant expression.
   3. A1>0 is always executed (is not control-dependent on anything);
      64 is data dependent on 63, wrt A1, which is the only, constant
      reaching definition.
3. Error # 3
   1. Depending on the decision in 64, A2 may be undefined at 70.
   2. A2 is not imported (not in In or In Out) but its INITIAL
      value may be used in 70b, as shown by A2 L 70b. In SPARK,
      relations L and The(eta) are used to identify only the direct,
      first use of undefined A2 in 70; the subsequent, chained uses
      (e.g. 71b) are not.
   3. 70 is data dependent on an dummy entry statement that makes each
      local variable undefined. Alternatively, A2 is live on entry, i.e.
      being used in 70 without a definition in between.
4. Error # 4
   As for #3, but the direct use involved refers to the loop body skipping path.
   Classical data dependency treats A2 defined in 70, although A2 defined there
   is so on the basis of an undefined variable.
5. Error # 5
   1. Definition of output Y in 74 uses potentially undefined A2.
   2. As in #3 and #4 above.
   3. No proscriptive warning possible without annotations, only descriptive.
6. Error # 6
   1. Assignment to B1 in 86 is not later used to compute the values of Out
      variables, i.e. X, Y, and Z.
   2. The expression 1 in 86.c is not related to any output variable under
      relation M.
   3. No statement assigning value to an output variables is data dependent
      on statement 86.c.
7. Error # 7 As in 6.
8. Error # 8 As in 6.
9. Error # 9
   1. The derived annotation does not list N as being used to derive Y.
      However, there two possibilities for N to be used in the derivation
      of Y. First, the loop uses D/=0, with initial D=N; depending on the
      test outcome, two different values of A2 in 116.b are possible. Second,
      within the loop, there is a chain of of uses/definitions:
      
      108. (N->D); 110 (D->Q); 112 (Q->A2); 113b (A2 -> A1);
      Second iteration: 113 (A1 -> T); 113c (T ->A2);
      Loop exit, use of A2 in 116b.
      
   2. Annotation checked against relation R.
   3. Without annotations, the fact that N may be used in the derivation of Y
      (actually always is) can be generated only as a descriptive, rather
      than proscriptive, message. It involves both control dependence and data
      dependence.
10. Error # 10
    1. If Event is neither Warning nor Advisory, an undefined value of
       Result may occur.
    2. (Result R Result) for the entire function, with Result being local.
    3. 133 depends on an intial dummy statement that sets all local
       variables undefined. Then 113 depends on such a statement.
11. Error # 11
    As in 10, except that an undefined Result may be returned.