CVS difference for ai12s/ai12-0112-1.txt
--- ai12s/ai12-0112-1.txt 2020/04/22 01:00:05 1.25
+++ ai12s/ai12-0112-1.txt 2020/05/29 02:18:13 1.26
@@ -2611,9 +2611,9 @@
@xcode< @b<procedure> Move (Target : @b<in out> Holder; Source : @b<in out> Holder);>
@dby
@xcode< @b<procedure> Move (Target : @b<in out> Holder; Source : @b<in out> Holder)
- @b<with> Pre =@> ((@b<not> Tampering_With_The_Element_Prohibited (Target))
+ @b<with> Pre =@> (@b<not> Tampering_With_The_Element_Prohibited (Target)
@b<or else raise> Program_Error) @b<and then>
- ((@b<not> Tampering_With_The_Element_Prohibited (Source))
+ (@b<not> Tampering_With_The_Element_Prohibited (Source)
@b<or else raise> Program_Error),
Post =@> (@b<if> Target /= Source @b<then>
Is_Empty (Source) @b<and then> (@b<not> Is_Empty (Target)));>
@@ -2625,9 +2625,9 @@
@xcode<@b<procedure> Move (Target : @b<in out> Holder; Source : @b<in out> Holder);>
@dby
@xcode<@b<procedure> Move (Target : @b<in out> Holder; Source : @b<in out> Holder)
- @b<with> Pre =@> ((@b<not> Tampering_With_The_Element_Prohibited (Target))
+ @b<with> Pre =@> (@b<not> Tampering_With_The_Element_Prohibited (Target)
@b<or else raise> Program_Error) @b<and then>
- ((@b<not> Tampering_With_The_Element_Prohibited (Source))
+ (@b<not> Tampering_With_The_Element_Prohibited (Source)
@b<or else raise> Program_Error),
Post =@> (@b<if> Target /= Source @b<then>
Is_Empty (Source) @b<and then> (@b<not> Is_Empty (Target)));>
Questions? Ask the ACAA Technical Agent