-
Notifications
You must be signed in to change notification settings - Fork 0
/
calculator.ads
156 lines (126 loc) · 5.49 KB
/
calculator.ads
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
with Ada.Containers; use Ada.Containers;
with VariableStore; use VariableStore;
with PIN;
with Stack;
with MyString;
package Calculator with
SPARK_Mode
is
type Calculator is private;
procedure Init (C : out Calculator; P : in PIN.PIN) with
Post => PIN."=" (Get_Pin (C), P) and Is_Locked (C) = True;
procedure Lock (C : in out Calculator; P : in PIN.PIN) with
Pre => not Is_Locked (C),
Post =>
Stack."=" (Get_Stack (C), Get_Stack (C'Old)) and
((not Is_Locked (C'Old) and PIN."=" (Get_Pin (C), P)) or
Is_Locked (C'Old) = True) and
Is_Locked (C) = True;
procedure Unlock (C : in out Calculator; P : in PIN.PIN) with
Pre => Is_Locked (C),
Post =>
PIN."=" (Get_Pin (C), Get_Pin (C'Old)) and
Stack."=" (Get_Stack (C), Get_Stack (C'Old)) and
((PIN."=" (Get_Pin (C), P) and Is_Locked (C) = False) or
(not PIN."=" (Get_Pin (C), P) and Is_Locked (C) = True));
procedure Plus (C : in out Calculator) with
Pre => not Is_Locked (C),
Post =>
PIN."=" (Get_Pin (C), Get_Pin (C'Old)) and
Is_Locked (C) = Is_Locked (C'Old) and
-- enough inputs => try operation
((Get_Stack (C'Old).Length >= 2 and
(Get_Stack (C).Length = Get_Stack (C'Old).Length - 1 or
Get_Stack (C).Length = Get_Stack (C'Old).Length)) or
-- not enough inputs => do nothing
(Get_Stack (C'Old).Length < 2 and
Stack."=" (Get_Stack (C), Get_Stack (C'Old))));
procedure Minus (C : in out Calculator) with
Pre => not Is_Locked (C),
Post =>
PIN."=" (Get_Pin (C), Get_Pin (C'Old)) and
Is_Locked (C) = Is_Locked (C'Old) and
-- enough inputs => try operation
((Get_Stack (C'Old).Length >= 2 and
(Get_Stack (C).Length = Get_Stack (C'Old).Length - 1 or
Get_Stack (C).Length = Get_Stack (C'Old).Length)) or
-- not enough inputs => do nothing
(Get_Stack (C'Old).Length < 2 and
Stack."=" (Get_Stack (C), Get_Stack (C'Old))));
procedure Multiply (C : in out Calculator) with
Pre => not Is_Locked (C),
Post =>
PIN."=" (Get_Pin (C), Get_Pin (C'Old)) and
Is_Locked (C) = Is_Locked (C'Old) and
-- enough inputs => try operation
((Get_Stack (C'Old).Length >= 2 and
(Get_Stack (C).Length = Get_Stack (C'Old).Length - 1 or
Get_Stack (C).Length = Get_Stack (C'Old).Length)) or
-- not enough inputs => do nothing
(Get_Stack (C'Old).Length < 2 and
Stack."=" (Get_Stack (C), Get_Stack (C'Old))));
procedure Divide (C : in out Calculator) with
Pre => not Is_Locked (C),
Post =>
PIN."=" (Get_Pin (C), Get_Pin (C'Old)) and
Is_Locked (C) = Is_Locked (C'Old) and
-- enough inputs => try operation
((Get_Stack (C'Old).Length >= 2 and
(Get_Stack (C).Length = Get_Stack (C'Old).Length - 1 or
Get_Stack (C).Length = Get_Stack (C'Old).Length)) or
-- not enough inputs => do nothing
(Get_Stack (C'Old).Length < 2 and
Stack."=" (Get_Stack (C), Get_Stack (C'Old))));
procedure Push (C : in out Calculator; I : Integer) with
Pre => not Is_Locked (C),
Post =>
PIN."=" (Get_Pin (C), Get_Pin (C'Old)) and
Is_Locked (C) = Is_Locked (C'Old) and
(Get_Stack (C).Length - 1 = Get_Stack (C'Old).Length or
Get_Stack (C).Length = Get_Stack (C'Old).Length);
procedure Pop (C : in out Calculator) with
Pre => not Is_Locked (C),
Post =>
PIN."=" (Get_Pin (C), Get_Pin (C'Old)) and
Is_Locked (C) = Is_Locked (C'Old);
procedure Load (C : in out Calculator; V : VariableStore.Variable) with
Pre => not Is_Locked (C),
Post =>
PIN."=" (Get_Pin (C), Get_Pin (C'Old)) and
Is_Locked (C) = Is_Locked (C'Old) and
(Stack."=" (Get_Stack (C), Get_Stack (C'Old)) or
Get_Stack (C).Length - 1 = Get_Stack (C'Old).Length);
procedure Store (C : in out Calculator; V : VariableStore.Variable) with
Pre => not Is_Locked (C),
Post =>
PIN."=" (Get_Pin (C), Get_Pin (C'Old)) and
Is_Locked (C) = Is_Locked (C'Old) and
-- enough inputs => try operation
((Get_Stack (C'Old).Length >= 1 and
(Get_Stack (C).Length = Get_Stack (C'Old).Length - 1 or
Get_Stack (C).Length = Get_Stack (C'Old).Length)) or
-- not enough inputs => do nothing
(Get_Stack (C'Old).Length < 1 and
Stack."=" (Get_Stack (C), Get_Stack (C'Old))));
procedure Remove (C : in out Calculator; V : VariableStore.Variable) with
Pre => not Is_Locked (C),
Post =>
PIN."=" (Get_Pin (C), Get_Pin (C'Old)) and
Is_Locked (C) = Is_Locked (C'Old) and
Stack."=" (Get_Stack (C), Get_Stack (C'Old));
procedure List (C : in Calculator) with
Global => null, Pre => Is_Locked (C) = False;
function Is_Locked (C : in Calculator) return Boolean;
function Get_Pin (C : in Calculator) return PIN.PIN;
function Get_Stack (C : in Calculator) return Stack.Stack;
private
type Calculator is record
St : Stack.Stack;
DB : VariableStore.Database;
P : PIN.PIN;
Locked : Boolean;
end record;
function Is_Locked (C : in Calculator) return Boolean is (C.Locked);
function Get_Pin (C : in Calculator) return PIN.PIN is (C.P);
function Get_Stack (C : in Calculator) return Stack.Stack is (C.St);
end Calculator;