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! ------ --Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--