Re: The future of Spark . Spark 2014 : a wreckage

[Stefan.Lucks@uni-weimar.de]

[-- Attachment #1: Type: TEXT/PLAIN, Size: 2463 bytes --]

On Mon, 8 Jul 2013, Peter C. Chapin wrote:

> On 07/08/2013 01:56 PM, vincent.diemunsch@gmail.com wrote:
>
>>     procedure Swap
>>        with Global  => (In_Out => (X, Y)),
>>             Depends => (X => Y,   -- to be read as "X depends on Y"
>>                         Y => X);  -- to be read as "Y depends on X"
>> 
>> How are we supposed to guess that "X => Y" means X depends on Y, if the 
>> arrow goes from X to Y ?
>
> Well the phrase "X depends on Y" has X on the left and Y on the right just as 
> X => Y does. So it reads fairly naturally to me. I understand there is value 
> in being consistent with existing notations although I get the impression 
> there is already conflicting practice in that area.
>
> More significantly, though, I think you may be assigning too much semantic 
> weight to the '=>' token in this case. In the aspect syntax it is used more 
> as a separator than anything else. Consider
>
>  Pre => X < 0

Fair enough! The "=>" is not an arrow, it is just a syntactic token to 
separate two other tokens.

Unfortunately, this token greatly (and certainly intentionally, at the 
early days of Ada) resembles an arrow. And this is relly confusing in 
situations where an arrow would make sense, but where the "=>" goes into 
the wrong direction. "Pre =>" isn't an issue, but X => Y above is.

Actually, this has been irritating me when using named notation for out 
parameters, since I have learned Ada. If Y is an out parameter, it should 
be Do_Something (X <= Y), shouldn't it?

This isn't such a big issue that Ada will actually need another separator 
token, such as "<=" ... we'll have to live with "=>". But maybe, one could 
turn this "bug" into a feature, by defining an alternative to the Depends 
annotation^H^H^H^H^H^H^H^H^H^H aspect, where the "=>" points into the 
correct direction, e.g.:

      procedure Swap
         with Global           => (In_Out => (X, Y)),
              Information_Flow => (Y => X,   -- "X depends on Y"
                                   X => Y);  -- "Y depends on X"

as a legal replacement for the usage of "Depends". That would be a lot 
more intuitive!

Alas, it is probably too late for SPARK 2014 ... sigh!


------  I  love  the  taste  of  Cryptanalysis  in  the morning!  ------
     <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
--Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--