CVS difference for ai12s/ai12-0339-1.txt
--- ai12s/ai12-0339-1.txt 2020/08/28 03:25:17 1.7
+++ ai12s/ai12-0339-1.txt 2021/06/03 02:16:53 1.8
@@ -606,10 +606,10 @@
@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;>
+ 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.
@@ -623,10 +623,10 @@
@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;>
+ 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.>
@@ -665,9 +665,9 @@
@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<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.
@@ -702,9 +702,9 @@
@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;>
+ 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.
@@ -756,8 +756,8 @@
@xcode< @b<function> Empty @b<return> Set
@b<is> (Empty_Set)
@b<with> Post =@>
- @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
- Length (Empty'Result) = 0;>
+ @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.
Questions? Ask the ACAA Technical Agent