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.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no 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.227.40 with SMTP id rx8mr9334356pbc.5.1328465061049; Sun, 05 Feb 2012 10:04:21 -0800 (PST) Path: lh20ni263965pbb.0!nntp.google.com!news1.google.com!news.glorb.com!dedekind.zen.co.uk!zen.net.uk!hamilton.zen.co.uk!prichard.zen.co.uk.POSTED!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: Silly and stupid post-condition or not ? Date: Sun, 5 Feb 2012 18:04:20 -0000 Message-ID: References: <82wr86fzos.fsf@stephe-leake.org> <5af407fc-2868-44ca-84d2-c51a2a64104d@o4g2000pbc.googlegroups.com> <82k445fu9n.fsf@stephe-leake.org> MIME-Version: 1.0 User-Agent: MicroPlanet-Gravity/3.0.4 Organization: Zen Internet NNTP-Posting-Host: b3e73c05.news.zen.co.uk X-Trace: DXC=j\lMV2DKJT70If2BDZ0j^=0g@SS;SF6n7R9OH0:RnEN4@79VK\HXa79gPN:7kYdTY;n@mRaDWK2E8 X-Complaints-To: abuse@zen.co.uk Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2012-02-05T18:04:20+00:00 List-Id: In article , bobduff@shell01.TheWorld.com says... > > 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. Yes - that's exactly what you *have* to do (not like) when you update two or more elements of an array (or prove your conclusion for either possibility of course). > 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 think that's a substantial point, the X and the Y can be expressions and that doesn't change anything. > > (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? My code is managing the list of free elements, as well as the elements in the data structure, so I need to show that every array element that should be in the free list is there and that there isn't any element in the free list that is also in the data structure. If I'm using access values then I'm relying on the correctness of the compiled code/Ada run- time handling of a storage pool, which probably has a lower level of integrity than I'm claiming for my code. But the main point I was making is that there doesn't seem to be any major benefits to the SPARK user from adding access values to the language. > > ... > SPARK may be great for certain types of systems, but I wouldn't > want to write (say) a compiler in SPARK. (Personally I wouldn't want to write a compiler at all .....) Phil