CVS difference for ai12s/ai12-0339-1.txt
--- ai12s/ai12-0339-1.txt 2019/07/20 00:59:46 1.4
+++ ai12s/ai12-0339-1.txt 2019/11/09 04:57:41 1.5
@@ -499,10 +499,11 @@
@xcode< @b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
@b<return> Vector
@b<with> Pre =@> (@b<if> Capacity @> Maximum_Length @b<then raise> Constraint_Error),
- Post =@> Capacity (Empty'Result) @>= Capacity @b<and then>
- @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Length (Empty'Result) = 0;>
+ Post =@>
+ Capacity (Empty'Result) @>= Capacity @b<and then>
+ @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+ @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+ Length (Empty'Result) = 0;>
!comment A.18.2(78.2/5) not in corrigendum text.
@@ -562,9 +563,10 @@
@dinst
@xcode< @b<function> Empty @b<return> List
@b<is> (Empty_List)
- @b<with> Post =@> @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Length (Empty'Result) = 0;>
+ @b<with> Post =@>
+ @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+ @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+ Length (Empty'Result) = 0;>
!comment A.18.3(50.2/5) not in corrigendum text.
@@ -603,10 +605,11 @@
@dinst
@xcode< @b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
@b<return> Map
- @b<with> Post =@> Capacity (Empty'Result) @>= Capacity @b<and then>
- @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Length (Empty'Result) = 0;>
+ @b<with> Post =@>
+ Capacity (Empty'Result) @>= Capacity @b<and then>
+ @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+ @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+ Length (Empty'Result) = 0;>
!comment A.18.5(37.3/5) not in corrigendum text.
@@ -619,10 +622,11 @@
@dinss
@xcode<@b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
@b<return> Map
- @b<with> Post =@> Capacity (Empty'Result) @>= Capacity @b<and then>
- @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Length (Empty'Result) = 0;>
+ @b<with> Post =@>
+ Capacity (Empty'Result) @>= Capacity @b<and then>
+ @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+ @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+ Length (Empty'Result) = 0;>
@xindent<Returns an empty map.>
@@ -660,9 +664,10 @@
@dinst
@xcode< @b<function> Empty @b<return> Map
@b<is> (Empty_Map)
- @b<with> Post =@> @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Length (Empty'Result) = 0;>
+ @b<with> Post =@>
+ @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+ @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+ Length (Empty'Result) = 0;>
!comment A.18.6(51.4/5) not in corrigendum text.
@@ -696,9 +701,10 @@
@dinst
@xcode< @b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
@b<return> Set
- @b<with> Post =@> Capacity (Empty'Result) @>= Capacity @b<and then>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Length (Empty'Result) = 0;>
+ @b<with> Post =@>
+ Capacity (Empty'Result) @>= Capacity @b<and then>
+ @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+ Length (Empty'Result) = 0;>
!comment A.18.8(59.2/5) not in corrigendum text.
@@ -711,9 +717,10 @@
@dinst
@xcode<@b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
@b<return> Set
- @b<with> Post =@> Capacity (Empty'Result) @>= Capacity @b<and then>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Length (Empty'Result) = 0;>
+ @b<with> Post =@>
+ Capacity (Empty'Result) @>= Capacity @b<and then>
+ @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+ Length (Empty'Result) = 0;>
@xindent<Returns an empty set.>
@@ -748,9 +755,9 @@
@dinst
@xcode< @b<function> Empty @b<return> Set
@b<is> (Empty_Set)
- @b<with> Post =@> @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Length (Empty'Result) = 0;>
+ @b<with> Post =@>
+ @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+ Length (Empty'Result) = 0;>
!comment A.18.9(74.2/5) not in corrigendum text.
@@ -762,9 +769,10 @@
@dinst
@xcode< @b<function> Empty @b<return> Tree
@b<is> (Empty_Tree)
- @b<with> Post =@> @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Node_Count (Empty'Result) = 1;>
+ @b<with> Post =@>
+ @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+ @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+ Node_Count (Empty'Result) = 1;>
!corrigendum A.18.18(8/3)
@@ -774,8 +782,10 @@
@dinst
@xcode< @b<function> Empty @b<return> Holder
@b<is> (Empty_Holder)
- @b<with> Post =@> @b<not> Tampering_With_The_Element_Prohibited (Empty'Result) @b<and then>
- Is_Empty (Empty'Result);>
+ @b<with> Post =@>
+ @b<not> Tampering_With_The_Element_Prohibited (Empty'Result)
+ @b<and then> Is_Empty (Empty'Result);>
+
!corrigendum A.18.19(6/3)
@@ -785,10 +795,11 @@
@dinss
@xbullet<In function Empty, the postcondition is altered to:>
-@xcode< Post =@> Empty'Result.Capacity = Capacity @b<and then>
- @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Length (Empty'Result) = 0;>
+@xcode< Post =@>
+ Empty'Result.Capacity = Capacity @b<and then>
+ @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+ @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+ Length (Empty'Result) = 0;>
!corrigendum A.18.20(6/3)
@@ -800,10 +811,11 @@
@xcode< @b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
@b<return> List
- @b<with> Post =@> Empty'Result.Capacity = Capacity @b<and then>
- @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Length (Empty'Result) = 0;>
+ @b<with> Post =@>
+ Empty'Result.Capacity = Capacity @b<and then>
+ @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+ @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+ Length (Empty'Result) = 0;>
!corrigendum A.18.21(6/3)
@@ -813,11 +825,12 @@
@dinss
@xbullet<In function Empty, the postcondition is altered to:>
-@xcode< Post =@> Empty'Result.Capacity = Capacity @b<and then>
- Empty'Result.Modulus = Default_Modulus (Capacity) @b<and then>
- @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Length (Empty'Result) = 0;>
+@xcode< Post =@>
+ Empty'Result.Capacity = Capacity @b<and then>
+ Empty'Result.Modulus = Default_Modulus (Capacity) @b<and then>
+ @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+ @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+ Length (Empty'Result) = 0;>
!corrigendum A.18.22(6/3)
@@ -829,10 +842,11 @@
@xcode< @b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
@b<return> Map
- @b<with> Post =@> Empty'Result.Capacity = Capacity @b<and then>
- @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Length (Empty'Result) = 0;>
+ @b<with> Post =@>
+ Empty'Result.Capacity = Capacity @b<and then>
+ @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+ @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+ Length (Empty'Result) = 0;>
!corrigendum A.18.23(6/3)
@@ -842,10 +856,11 @@
@dinss
@xbullet<In function Empty, the postcondition is altered to:>
-@xcode< Post =@> Empty'Result.Capacity = Capacity @b<and then>
- Empty'Result.Modulus = Default_Modulus (Capacity) @b<and then>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Length (Empty'Result) = 0;>
+@xcode< Post =@>
+ Empty'Result.Capacity = Capacity @b<and then>
+ Empty'Result.Modulus = Default_Modulus (Capacity) @b<and then>
+ @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+ Length (Empty'Result) = 0;>
!corrigendum A.18.24(6/3)
@@ -857,9 +872,10 @@
@xcode< @b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
@b<return> Set
- @b<with> Post =@> Empty'Result.Capacity = Capacity @b<and then>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Length (Empty'Result) = 0;>
+ @b<with> Post =@>
+ Empty'Result.Capacity = Capacity @b<and then>
+ @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+ Length (Empty'Result) = 0;>
!corrigendum A.18.25(6/3)
@@ -871,10 +887,11 @@
@xcode< @b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
@b<return> Tree
- @b<with> Post =@> Empty'Result.Capacity = Capacity @b<and then>
- @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Node_Count (Empty'Result) = 1;>
+ @b<with> Post =@>
+ Empty'Result.Capacity = Capacity @b<and then>
+ @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+ @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+ Node_Count (Empty'Result) = 1;>
!ASIS
Questions? Ask the ACAA Technical Agent