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=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,cbd507df3efa824b X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2001-02-01 05:21:57 PST Message-ID: <3A796150.9478111F@baesystems.com> Date: Thu, 01 Feb 2001 13:14:56 +0000 From: Stuart Palin Organization: BAE SYSTEMS Avionics, Rochester X-Mailer: Mozilla 4.5 [en] (WinNT; I) X-Accept-Language: en,pdf MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: SPARK flow analysis (was Help with Atomic_Components and whole array assignment) References: <94h55t$9a1$1@nnrp1.deja.com> <94hml1$o64$1@nnrp1.deja.com> <94hno6$p8s$1@nnrp1.deja.com> <3A76E455.AABF2490@averstar.com> <958o8f$vem$1@nnrp1.deja.com> <3A7886A7.F1BB5513@averstar.com> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit NNTP-Posting-Host: rc2966.rochstr.gmav.gecm.com X-Trace: 1 Feb 2001 13:08:43 GMT, rc2966.rochstr.gmav.gecm.com Path: supernews.google.com!sn-xit-02!supernews.com!news.tele.dk!193.190.198.17!newsfeeds.belnet.be!news.belnet.be!btnet-peer1!btnet-peer0!btnet-feed5!btnet!newreader.ukcore.bt.net!pull.gecm.com!rc2966.rochstr.gmav.gecm.com Xref: supernews.google.com comp.lang.ada:4817 Date: 2001-02-01T13:14:56+00:00 List-Id: Tucker Taft wrote: > Rod Chapman wrote: > > The assignment > > A := A_Type'(others => 0); > > has information flow "derives A from ;" (i.e. the final value of > > A is derived from "nothing" - a constant - which is probably what > > you wanted and expected) > > > > The compound statement > > for I in A'Range loop > > A(I) := 0; > > end loop; > > has information flow "derives A from A", which is significantly > > different. > > I don't understand why this derives A from A. Is this just > a limitation of SPARK? Clearly, we are assigning a new > value to every component of A, making no use of the original > values. You are correct in that in the overall scheme of things A does not derive from A, because in both cases A is entirely defined as 0. However, in the first case the fact that A is fully defined as 0 is obvious from the _syntax_ of the single statement; whereas in the second case it only becomes apparent from the _semantics_ of the set of statements. The SPARK Examiner analyses code at 2 levels; the less sophisticated of the two is Flow Analysis which reports on the apparent behaviour of a subprogram based upon the cumulative effects of statements, using only the simple syntactic properties of each statement. Despite being a "simpler" analysis it is still quite capable of detecting significant classes of faults, and the more the code behaviour is reflected in the syntax the better the analysis. (The value of flow analysis is that it can help eliminate many common programming errors before investing time and effort into creating proofs of correctness - or rather, if the program is flawed, failing to produce a proof and realising your mistake after many hours). Another example of syntax v semantics would be: if B then if B then x := 0; x := 0; else end if; x := 1; end if; if not B then x := 1; end if; In the left hand case the fact that x is only dependent on B is clear from the syntax; whereas in the right hand case this only becomes clear from the semantics (Flow analysis of the right hand case would suggest that x may depend on its original value as well as B. This is because until you examine the semantics and establish that if x has not been assigned the value 0 it must be assigned 1. Looking at the syntax alone suggests that there might be a path through the code in which x is never given a value (it also suggests there might be a path in which it is assigned the value 0 then, without that being used, it might be re-assigned the value 1: but that is a different story and a different warning). When you use SPARK to do semantic analysis and construct program proofs you would would be able to show that the two programs are equivalent. -- Stuart Palin Principal Software Engineer BAE SYSTEMS Avionics Ltd, Rochester