Re: Quantified Expressions: "some"

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

On 18.11.10 18:58, Peter C. Chapin wrote:

> John Barnes outlines his objection to the vertical bar in a message
> dated September 15, 2010. Two of his objections would also apply to ':'
> as well ("too weak a symbol" and "=> is better because SPARK uses the
> same symbol for the same purpose.")

More fun with arrows.  The AI started from the usual Such That (|) notation:

  (for all I in A'First .. T'Pred(A'Last) | A (I) <= A (T'Succ (I)))


With "=>" replacing "|", this becomes

  (for all I in A'First .. T'Pred(A'Last) => A (I) <= A (T'Succ (I)))

Slightly reformatted:

  (for all I in A'First .. T'Pred(A'Last)
      => A (I) <=
      A (T'Succ (I)))


This is nothing new, just venerable pointy syntax. There has always been,
for example, Boolean'Array (1 => 3 <= N).

But! The expression structure seems rather more likely now,
as it will appear frequently in Post aspects, one example being upper
bounds on a parameter.  The sequence of characters "=> X <=" is
a bit odd, because on the one hand, the "arrows" are so
close together, and symmetrical, but on the other hand, the readers
must doubly distinguish between them to understand the program;
doing so, they must be alert and

(a) know that "=>" is just an arrow for associations(*), and

(b) know that its very mirror, "<=" is defined at a very different
linguistic level, that of relational operators.

This *is* confusing (and is an opportunity for condescension of
Him Who Knows Ada Well), even though this piece of obfuscation is old,
if rarely used in the past.

I guess, then, one Would recommend a pair of parentheses:

  (for all I in A'First .. T'Pred(A'Last) => (A (I) <= A (T'Succ (I))))

OK.  However, by the same token, the pair could be used for "in (3 | 4)"
and Such That could stay as "|".

__
(*) better not to have written any Prolog recently...