From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.unit0.net!takemy.news.telefonica.de!telefonica.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Tue, 09 Jul 2013 13:13:36 +0200
From: "G.B." <rm-dash-bau-haus@dash.futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7;
 rv:17.0) Gecko/20130620 Thunderbird/17.0.7
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: The future of Spark . Spark 2014 : a wreckage
References: <d84b2eb2-eab3-4dec-917c-0498473c1e93@googlegroups.com>
 <87hag4ahu5.fsf@mid.deneb.enyo.de>
 <1rbbala6i0jcl$.dswyfcctu6vs$.dlg@40tude.net>
 <51dbca43$0$6572$9b4e6d93@newsspool3.arcor-online.net>
 <1gs2slsmkpvbf.a9h84b9jcowi$.dlg@40tude.net>
In-Reply-To: <1gs2slsmkpvbf.a9h84b9jcowi$.dlg@40tude.net>
Content-Type: text/plain; charset=Big5
Content-Transfer-Encoding: 8bit
Message-ID: <51dbf060$0$6569$9b4e6d93@newsspool3.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 09 Jul 2013 13:13:36 CEST
NNTP-Posting-Host: 03fa039b.newsspool3.arcor-online.net
X-Trace: 
 DXC=ZNf5Q]JBQL8Tia]Ho99G50McF=Q^Z^V384Fo<]lROoR18kF<OcfhCO;hN115;<XaX0nc\616M64>:Lh>_cHTX3j=Vfd3g8Z`Fc5
X-Complaints-To: usenet-abuse@arcor.de
Xref: news.eternal-september.org comp.lang.ada:16201
Date: 2013-07-09T13:13:36+02:00
List-Id: <comp.lang.ada>

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.