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 X-Received: by 10.180.187.229 with SMTP id fv5mr7004344wic.6.1373443315845; Wed, 10 Jul 2013 01:01:55 -0700 (PDT) Path: border1.nntp.dca3.giganews.com!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!mf3no13319850wib.1!news-out.google.com!md6ni51218wic.0!nntp.google.com!fu-berlin.de!news-1.dfn.de!news.dfn.de!news.uni-weimar.de!medsec1.medien.uni-weimar.de!lucks From: Stefan.Lucks@uni-weimar.de Newsgroups: comp.lang.ada Subject: Re: The future of Spark . Spark 2014 : a wreckage Date: Wed, 10 Jul 2013 10:03:21 +0200 Organization: Bauhaus-Universitaet Weimar Message-ID: References: NNTP-Posting-Host: medsec1.medien.uni-weimar.de Mime-Version: 1.0 X-Trace: tigger.scc.uni-weimar.de 1373443315 21220 141.54.178.228 (10 Jul 2013 08:01:55 GMT) X-Complaints-To: news@tigger.scc.uni-weimar.de NNTP-Posting-Date: Wed, 10 Jul 2013 08:01:55 +0000 (UTC) X-X-Sender: lucks@debian In-Reply-To: User-Agent: Alpine 2.10 (DEB 1266 2009-07-14) Content-Type: TEXT/PLAIN; CHARSET=ISO-8859-15; FORMAT=flowed Content-Transfer-Encoding: QUOTED-PRINTABLE Content-ID: X-Original-Lines: 118 X-Original-Bytes: 5693 Xref: number.nntp.dca.giganews.com comp.lang.ada:182418 Date: 2013-07-10T10:03:21+02:00 List-Id: On Tue, 9 Jul 2013, Randy Brukardt wrote: > wrote: >> So you think, information flow analysis is completely worthless? (I mean= , >> for building and verifying correct systems -- as a compiler writer you >> will not question the usage of information flow analysis inside the >> compiler or optimiser). > > Information flow *within* a subprogram is important. Information flow > *between* subprograms is completely defined by the subprogram's interface= s > and calls. Firstly, for current Ada (i.e., Ada 2012) this is completely wrong=20 whenever a program manipulates global variables. Even specifying pre- and= =20 postconditions doesn't guarantee the absence of any other (side-)effects. (You are right, however, a proper "global" annotation would seem to catch= =20 this.) Secondly, Ada's "in", "out", and "in out" information give only a cursory= =20 view of what is going on. Even *without* pre- and postcondition, verifying= =20 a SPARK-like specification of, say, procedure Count_Vote(Vote: Vote_Type; Count_A, Count_B, Invalid: out Natural) =09with Depends (Count_A =3D> Vote, Count_A, Count_B =3D> Vote, Count_B, Invalid =3D> Vote, Invalid); give a great deal of assurance -- a lot more than the same specification=20 without the Depends Aspect. Now consider the following not-quite-complete contract with pre- and=20 postconditions: procedure Count_Vote(Vote: Vote_Type; Count_A, Count_B, Invalid: out Natural) =09with Pre =3D> ((Count_A <=3D Natural'Last) and =09 (Count_B <=3D Natural'Last) and (Count_C <=3D Natural'Last)), Post =3D> ((Count_A >=3D Count_A'Old) and (Count_B >=3D Count_B'Old) and (Invalid >=3D Invalid'Old) and (Count_A + Count_B + Invalid =3D =09 (Count_A + Count_B + Invalid)'Old +1); At a first look, this may appear to be more precise. Each vote will=20 increase exactly one counter, either Count_A or Count_B or Invalid. All=20 what is left open is how does Count_Vote decide about which counter to=20 increase. However, a correct (up to the specification) implementation could do the=20 following: procedure Count_Vote(Vote: Vote_Type; Count_A, Count_B, Invalid: out Natural) is begin if (Vote =3D 'A') or (Vote=3D'a') then =09Count_A :=3D Count_A + 1; elsif (Vote =3D 'B') or (Vote=3D'b') then if (Count_A + Count_B < 1000) or else Count_B < Count_A then Count_B :=3D Count_B + 1; else Count_A :=3D Count_A + 1; -- Make sure A wins, assuming more than 2000 valid votes. end if; else Invalid :=3D Invalid + 1; end if; end Count_Vote; Without "Depends", your cool analysis tool verifying all pre- and=20 postconditions will not catch this bug. And yes, I am aware that another=20 implementation could cheat without violating the "Depends" clause. But=20 ensuring an "innocent" result (a marginal lead for A where the real result= =20 would be a marginal lead for B) would be a lot more difficult, if not=20 impossible. The above is a malicious example, but the "frame problem" is a big issue=20 for program analysis in general. It appears to be fairly difficult to=20 write pre- and postconditions such that you can be sure nothing else is=20 going on. "Global" and "Depends" allow to make "nothing else" claims that= =20 analysis tools can actually verify and use for their subsequent analysis,= =20 and where "Depends" is a lot more specific than "Global". > Other information ought to be irrelevant (no one should be > depending upon what the body of Swap does, other than whatever is specifi= ed > in the postcondition). I agree that no one should depend on what the body of some Subprogram=20 does. But then, information flow analysis is actually useful! ------ I love the taste of Cryptanalysis in the morning! ------ --Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universit=E4t Weimar, Germany--