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