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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no 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!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: The future of Spark . Spark 2014 : a wreckage Date: Tue, 9 Jul 2013 10:58:17 +0200 Organization: cbb software GmbH Message-ID: <1gs2slsmkpvbf.a9h84b9jcowi$.dlg@40tude.net> References: <87hag4ahu5.fsf@mid.deneb.enyo.de> <1rbbala6i0jcl$.dswyfcctu6vs$.dlg@40tude.net> <51dbca43$0$6572$9b4e6d93@newsspool3.arcor-online.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: IenaDxMXK2hi7fvYcb+MlQ.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset="big5" Content-Transfer-Encoding: 8bit X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:16197 Date: 2013-07-09T10:58:17+02:00 List-Id: 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