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

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

On 09.07.13 09:40, Dmitry A. Kazakov wrote:
> On Mon, 08 Jul 2013 22:59:30 +0200, Florian Weimer wrote:
>
>> * vincent diemunsch:
>>
>>> Same specification in Spark 2014 :
>>>     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 ? In the literature, Flow analysis use
>>> always Information Flow where arrows follows the real move of
>>> information. See for instance "SPARK the proven approach of High
>>> Integrity Software" from John Barn page 311 or the "Dragon Book"
>>> (Compilers : principles, techniques and tools).
>>
>> This is nothing new.  Boolean implication p → q is already written as
>> P <= Q in Ada.
>
> Where?

In Boolean expressions. With obvious, I think, abbreviations
and referring to ordering of (False, True), and (0, 1),

p q | p → q   (p <= q)
-----------------------
1 1 |   1       True
1 0 |   0       False
0 1 |   1       True
0 0 |   1       True