@@ -127,38 +127,38 @@ Quiz
127127
128128 .. code :: Ada
129129
130- package Counter_System is
131- type Counter_T is private;
132- procedure Increment (Val_To_Inc :
133- in out Counter_T);
130+ package Counter is
131+ type Count_T is private;
132+ procedure Increment (Val : in out Count_T);
134133 private
135- function Is_Valid (Val_To_Check : Integer)
136- return Boolean;
137- type Counter_T is new Integer with
138- Type_Invariant => Is_Valid (Integer (Counter_T));
139- end Counter_System;
140-
141- package body Counter_System is
142- function Increment_Helper (Helper_Num : Counter_T)
143- return Counter_T is
144- New_Val : Counter_T := Helper_Num + 1;
134+ function Check_Limit (Value : Integer)
135+ return Boolean;
136+ type Count_T is new Integer with
137+ Type_Invariant =>
138+ Check_Limit (Integer (Count_T));
139+ end Counter;
140+
141+ package body Counter is
142+ function Increment_Helper
143+ (Helper_Val : Count_T)
144+ return Count_T is
145+ Next_Value : Count_T := Helper_Val + 1;
145146 begin
146- return New_Val ;
147+ return Next_Value ;
147148 end Increment_Helper;
148- procedure Increment (Val_To_Inc :
149- in out Counter_T) is
149+ procedure Increment (Val : in out Count_T) is
150150 begin
151- Val_To_Inc := Val_To_Inc + 1;
152- Val_To_Inc := Increment_Helper (Val_To_Inc );
151+ Val := Val + 1;
152+ Val := Increment_Helper (Val );
153153 end Increment;
154- function Is_Valid (Val_To_Check : Integer)
155- return Boolean is
156- (True);
157- end Counter_System ;
154+ function Check_Limit (Value : Integer)
155+ return Boolean is
156+ (Value <= 100); -- check against constraint
157+ end Counter ;
158158
159159 .. container :: column
160160
161- If `Increment ` is called from outside of Counter_System , how many times is `Is_Valid ` called?
161+ If `Increment ` is called from outside of Counter , how many times is `Check_Limit ` called?
162162
163163 A. 1
164164 B. :answer: `2 `
@@ -167,8 +167,10 @@ Quiz
167167
168168 .. container :: animate
169169
170- Type Invariants are only evaluated on entry into and exit from
171- externally visible subprograms. So :ada: `Is_Valid ` is called when
172- entering and exiting :ada: `Increment ` - not :ada: `Increment_Helper `,
173- even though a new instance of :ada: `Counter_T ` is created
170+ Type Invariants are only evaluated on entry into/exit from
171+ externally visible subprograms. So :ada: `Check_Limit ` is called when
172+ entering/exiting :ada: `Increment ` - not :ada: `Increment_Helper `
174173
174+ .. raw :: latex
175+
176+ \vspace {5mm}
0 commit comments