--- ai05s/ai05-0176-1.txt 2011/03/04 00:40:43 1.22 +++ ai05s/ai05-0176-1.txt 2011/11/01 05:32:52 1.23 @@ -214,7 +214,7 @@ @fa<iterator_specification> is first elaborated. The evaluation of a @fa<quantified_expression> then evaluates the @fa<predicate> for each value of the loop parameter. These values are examined in the order specified by the @fa<loop_parameter_specification> (see 5.5) -or @fa<iterator_specification> (see 5.5.1). +or @fa<iterator_specification> (see 5.5.2). The value of the @fa<quantified_expression> is determined as follows: @@ -237,8 +237,8 @@ The postcondition for a sorting routine on an array A with an index subtype T can be written: -@xcode<Post =@> (A'Length < 2 - @b<or else> (@b<for all> I @b<in> A'First .. T'Pred(A'Last) =@> A (I) <= A (T'Succ (I))))> +@xcode<Post =@> (A'Length < 2 @b<or else> + (@b<for all> I @b<in> A'First .. T'Pred(A'Last) =@> A (I) <= A (T'Succ (I))))> The assertion that a positive number is composite (as opposed to prime) can be written:

Questions? Ask the ACAA Technical Agent