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

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

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?

It would be plain wrong, because logical implication (not P or Q) must be
denoted as P => Q.

   http://en.wikipedia.org/wiki/Material_conditional

BTW, there is a difference between implication (Boolean operation) and
consequence like

   P |= Q

   http://en.wikipedia.org/wiki/Logical_consequence#Semantic_consequence

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de