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


                       DATE : 09-MAR-2010 15:43:31.93

Line
   1  package body Stack
   2     --# own State is Pointer, Vector; -- rappresentazione
   3  is
   4     StackSize : constant Integer := 100; --
   5  
   6     -- subtype Natural is Integer range 0 .. Integer'Last;
   7     -- subtype Positive is NaturalT range 1 .. Natural'Last;
   8  
   9     subtype PointerT is Natural range Natural'First .. StackSize;
  10  
  11     Pointer : PointerT;
  12  
  13     type IntVectorT is array (Integer range <>) of Integer;
  14     subtype StackIndexRange is Positive range 1 .. StackSize;
  15     subtype IntStackT is IntVectorT (StackIndexRange);
  16  
  17     Vector : IntStackT;
  18  
  19     EmptyVector : constant IntStackT := IntStackT'(StackIndexRange => 0);
  20  
  21     -----------
  22     -- Empty --
  23     -----------
  24  
  25     function Empty return Boolean
  26     --# global Pointer;
  27     is
  28     begin
  29        return Pointer = 0; -- and IntVector'First = 0 ; --and IntVectorT'First = 0
  30     end Empty;

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

  31  
  32     -----------
  33     -- Clear --
  34     -----------
  35  
  36     procedure Clear
  37     --# global out Pointer, Vector;
  38     --# derives Pointer, Vector from ;
  39     is
  40     begin
  41        Pointer := 0;
  42        Vector  := EmptyVector;
  43     end Clear;

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

  44  
  45     ---------
  46     -- Pop --
  47     ---------
  48  
  49     procedure Pop (X : out Integer)
  50     --# global in out Pointer; in Vector; -- Vector non è modificato!
  51     --# derives Pointer from *            -- ma State sì.
  52     --# &             X from Pointer, Vector;
  53     is
  54     begin
  55        X := Vector(Pointer);
  56        Pointer := Pointer - 1;
  57     end Pop;

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

  58  
  59     ----------
  60     -- Push --
  61     ----------
  62  
  63     procedure Push (X : in Integer)
  64     --# global in out Pointer, Vector;
  65     --# derives Pointer from *
  66     --# &        Vector from *, Pointer, X;
  67     is
  68     begin
  69        Pointer := Pointer + 1;
  70        Vector(Pointer) := X;
  71     end Push;

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

  72  
  73     function Sum (A : in IntStackT) return Integer
  74     is
  75        Result : Integer := 0;
  76     begin
  77        cicle:
  78        for I in StackIndexRange loop --  in IntStackT'Range  non va bene!
  79           Result := Result + A(I);
  80        end loop cicle;
  81        return Result;
  82     end Sum;

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

  83  
  84  --     function SumAda (A : in IntVectorT) return Integer
  85  --     is
  86  --        Low : Integer := 1;
  87  --        Result : Integer := 0;
  88  --     begin
  89  --        cicle:
  90  --        for I in A'Range loop  -- non passa Examiner
  91  --           Result := Result + A(I);
  92  --        end loop cicle;
  93  --        return Result;
  94  --     end SumAda;
  95  
  96     function SumSPARK (A : in IntVectorT) return Integer
  97     is
  98        I : Integer ;
  99        High : Integer ;
 100        Result : Integer := 0;
 101     begin
 102        I := A'First;
 103        High := A'Last;
 104        cicle:
 105        while I <= High loop
 106           Result := Result + A(I);
 107           I := I+1;
 108        end loop cicle;
 109        return Result;
 110     end SumSPARK;

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

 111  
 112     function SumSPARK2 (A : in IntVectorT) return Integer
 113     is
 114        I : Integer ;
 115        High : Integer ;
 116        Result : Integer := 0;
 117     begin
 118        I := A'First;
 119        High := A'Last;
 120        cicle: loop -- while I <= High
 121           exit cicle when I > High;
 122           Result := Result + A(I);
 123           I := I+1;
 124        end loop cicle;
 125        return Result;
 126     end SumSPARK2;

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

 127  
 128  begin
 129        Pointer := 0;
 130        Vector  := EmptyVector;
 131  end Stack;

+++        Flow analysis of package initialization 
           performed: no errors found.



--End of file--------------------------------------------------