@@ -113,9 +113,9 @@ Example: A String Holder (1/2)
113
113
package String_Holders is
114
114
type Info is limited private;
115
115
116
- function Contains (I : Info; S : String) return Boolean
116
+ function Contains (Obj : Info; Str : String) return Boolean
117
117
with Ghost;
118
- function Equals (A, B : Info) return Boolean
118
+ function Equals (Left, Right : Info) return Boolean
119
119
with Ghost;
120
120
121
121
.. tip ::
@@ -124,7 +124,7 @@ Example: A String Holder (1/2)
124
124
125
125
.. code :: Ada
126
126
127
- function To_Info (S : String) return Info
127
+ function To_Info (Str : String) return Info
128
128
with Post => Contains (To_Info'Result, S);
129
129
130
130
function To_String (Obj : Info)
@@ -136,7 +136,7 @@ Example: A String Holder (1/2)
136
136
with Post => Equals (To, From);
137
137
138
138
procedure Append (Obj : in out Info;
139
- S : String)
139
+ Str : String)
140
140
with Post => Contains (Obj, To_String (Obj)'Old & S);
141
141
142
142
procedure Destroy (Obj : in out Info);
@@ -150,15 +150,15 @@ Example: A String Holder (2/2)
150
150
private
151
151
type Info is access String;
152
152
153
- function To_String_Internal (I : Info) return String
154
- is (if I = null then "" else I .all);
153
+ function To_String_Internal (Obj : Info) return String
154
+ is (if Obj = null then "" else Obj .all);
155
155
.. tip ::
156
156
157
157
This can be used by contracts implementation below, and child packages
158
158
159
159
.. code :: Ada
160
160
161
- function Contains (I : Info; S : String) return Boolean
162
- is (I /= null and then I .all = S );
163
- function Equals (A, B : Info) return Boolean
164
- is (To_String_Internal (A ) = To_String_Internal (B ));
161
+ function Contains (Obj : Info; Str : String) return Boolean
162
+ is (Obj /= null and then Obj .all = Str );
163
+ function Equals (Left, Right : Info) return Boolean
164
+ is (To_String_Internal (Left ) = To_String_Internal (Right ));
0 commit comments