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.73.229 with SMTP id o5mr9582818pbv.7.1328477247428; Sun, 05 Feb 2012 13:27:27 -0800 (PST) Path: lh20ni264478pbb.0!nntp.google.com!news1.google.com!newsfeed2.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 16:27:26 -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 1328477246 14374 192.74.137.71 (5 Feb 2012 21:27:26 GMT) X-Complaints-To: abuse@TheWorld.com NNTP-Posting-Date: Sun, 5 Feb 2012 21:27:26 +0000 (UTC) User-Agent: Gnus/5.1008 (Gnus v5.10.8) Emacs/21.3 (irix) Cancel-Lock: sha1:x2gQD/wJ9g2/dbVTDN81DX0e65o= Content-Type: text/plain; charset=us-ascii Date: 2012-02-05T16:27:26-05:00 List-Id: Phil Thornley writes: > In article , > bobduff@shell01.TheWorld.com says... >> 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 meant that things like "X := X + 1;" changes what X points at. That's allowed for indices, but not for pointers. Suppose you want to know what might be modified by procedure P, and P takes a parameter X that's a (pointer to a) linked list. I'm not necessarily talking about SPARK, here. I (or some tool) can reason that P can only modify what X points at (transitively). But if X is an index, and we're using some array as a hand-made "heap", it's as if every heap object points to every other heap object (including ones on the free list!), because P can say X+1, X+2, X-1, etc. OTOH, I suppose making it a private type helps. >> 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. I see. Thanks. >...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. True, although there are user-defined storage pools in Ada (not in SPARK). > (Personally I wouldn't want to write a compiler at all .....) Writing a bootstrapped compiler is the coolest thing in the world. ;-) - Bob