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

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

On Tue, 09 Jul 2013 10:30:59 +0200, Georg Bauhaus wrote:

> 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

This is p=>q

    p=>q  =def=  not p or q
/= q=>p  =def=  not q or p

p<=q = q=>p is

p q | p<=q
----------
1 1 | 1
1 0 | 1
0 1 | 0
0 0 | 1

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