******************************************************* 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--------------------------------------------------