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: 
 border1.nntp.ams3.giganews.com!border1.nntp.ams2.giganews.com!border2.nntp.ams2.giganews.com!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!nntp.giganews.com!feeder.erje.net!eu.feeder.erje.net!news.szaf.org!news.gnuher.de!news.enyo.de!.POSTED!not-for-mail
From: Florian Weimer <fw@deneb.enyo.de>
Newsgroups: comp.lang.ada
Subject: Re: The future of Spark . Spark 2014 : a wreckage
Date: Mon, 08 Jul 2013 22:59:30 +0200
Message-ID: <87hag4ahu5.fsf@mid.deneb.enyo.de>
References: <d84b2eb2-eab3-4dec-917c-0498473c1e93@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
X-Trace: news.enyo.de 1373317141 19345 172.17.135.6 (8 Jul 2013 20:59:01 GMT)
X-Complaints-To: news@enyo.de
Cancel-Lock: sha1:rEEJWCKHp2JKLYvE4MkCPfPMSBk=
X-Original-Bytes: 1455
Xref: number.nntp.dca.giganews.com comp.lang.ada:182344
Date: 2013-07-08T22:59:30+02:00
List-Id: <comp.lang.ada>

* 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.