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!newsfeed.datemas.de!uucp.gnuu.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Tue, 09 Jul 2013 10:30:59 +0200 From: Georg Bauhaus 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: <87hag4ahu5.fsf@mid.deneb.enyo.de> <1rbbala6i0jcl$.dswyfcctu6vs$.dlg@40tude.net> In-Reply-To: <1rbbala6i0jcl$.dswyfcctu6vs$.dlg@40tude.net> Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Message-ID: <51dbca43$0$6572$9b4e6d93@newsspool3.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 09 Jul 2013 10:30:59 CEST NNTP-Posting-Host: 299dc918.newsspool3.arcor-online.net X-Trace: DXC=L6Q?P5=A:4lIkjb;<8iR=aMcF=Q^Z^V3h4Fo<]lROoRa8kFejVhEJ0JIOO5>Fb1=]g9>2Do3l X-Complaints-To: usenet-abuse@arcor.de Xref: news.eternal-september.org comp.lang.ada:16195 Date: 2013-07-09T10:30:59+02:00 List-Id: 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