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

["G.B." <rm-dash-bau-haus@dash.futureapps.de>]

On 09.07.13 10:58, Dmitry A. Kazakov wrote:
> 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

"Boolean implication p → q is already written as
 P <= Q in Ada."

As shown above. "=>" has no "Boolean" meaning in Ada.
(It has, in Prolog.) In implementation defined aspects,
GNAT is free to assign "depends" to "=>", UML style.

I guess we need to adapt to even more overloadings,
since symbolophobia is part of Ada culture.