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-Thread: 103376,ad06d2d7cb045687 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.74.201 with SMTP id w9mr4108120pbv.0.1328454193755; Sun, 05 Feb 2012 07:03:13 -0800 (PST) Path: lh20ni263514pbb.0!nntp.google.com!news2.google.com!newsfeed2.dallas1.level3.net!newsfeed3.dallas1.level3.net!news.level3.com!bloom-beacon.mit.edu!newsswitch.lcs.mit.edu!nntp.TheWorld.com!not-for-mail From: Robert A Duff Newsgroups: comp.lang.ada Subject: Re: Silly and stupid post-condition or not ? Date: Sun, 05 Feb 2012 10:03:12 -0500 Organization: The World Public Access UNIX, Brookline, MA Message-ID: References: <82wr86fzos.fsf@stephe-leake.org> <5af407fc-2868-44ca-84d2-c51a2a64104d@o4g2000pbc.googlegroups.com> <82k445fu9n.fsf@stephe-leake.org> NNTP-Posting-Host: shell01.theworld.com Mime-Version: 1.0 X-Trace: pcls6.std.com 1328454193 4594 192.74.137.71 (5 Feb 2012 15:03:13 GMT) X-Complaints-To: abuse@TheWorld.com NNTP-Posting-Date: Sun, 5 Feb 2012 15:03:13 +0000 (UTC) User-Agent: Gnus/5.1008 (Gnus v5.10.8) Emacs/21.3 (irix) Cancel-Lock: sha1:D8LA/ysPoUg9/6w9kGRM9nJ1mWk= Content-Type: text/plain; charset=us-ascii Date: 2012-02-05T10:03:12-05:00 List-Id: Phil Thornley writes: > The original SPARK Rationale says: "All Ada features which require > dynamic storage allocation were ruled out, for several reasons. The > specification and modelling of access type manipulations, which can > involve aliasing, is extremely difficult; for programs using access > types it may also be very difficult to achieve security ..., let alone > verification." Yes, aliasing makes analysis very difficult. But... > Remember that everything in a SPARK program must have a name, and that > it is quite easy to implement dynamic storage for a single type by a > simple array (access value <-> array index). Yes, you can simulate pointers (access values) using arrays and indices. This introduces the same aliasing issues, and the same dangling pointer (dangling index) issues. A(X) can in general alias A(Y), and a compiler or analysis tool would like to prove X=Y, or prove X/=Y. It seems like the aliasing issue is harder with indices, because you can do arithmetic one them, whereas you can't do arithmetic on pointers (in Ada). (I don't see why this has anything to do with having names. And not "everything" must have a name, but I know what you mean.) >... Furthermore when dealing > with dynamically sized data structures the invariant typically needs to > include predicates for the storage space that is not currently in use as > well as the storage that is. I'm not sure what you mean by that. Could you give an example? > "Of course, the extent to which Ada must be simplified for high- > integrity programming will be a matter of opinion: ... Indeed. SPARK may be great for certain types of systems, but I wouldn't want to write (say) a compiler in SPARK. - Bob