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.7 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM,REPLYTO_WITHOUT_TO_CC 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.189.72 with SMTP id gg8mr9707791pbc.4.1328483343153;
        Sun, 05 Feb 2012 15:09:03 -0800 (PST)
Path: 
 lh20ni264735pbb.0!nntp.google.com!news2.google.com!goblin3!goblin1!goblin.stu.neva.ru!txtfeed2.tudelft.nl!tudelft.nl!txtfeed1.tudelft.nl!dedekind.zen.co.uk!zen.net.uk!hamilton.zen.co.uk!reader02.news.zen.co.uk.POSTED!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: Silly and stupid post-condition or not ?
Date: Sun, 5 Feb 2012 23:09:02 -0000
Message-ID: <MPG.29991c6d55017731989685@news.zen.co.uk>
References: <op.v8w6ptk5ule2fv@douda-yannick>
 <82wr86fzos.fsf@stephe-leake.org>
 <5af407fc-2868-44ca-84d2-c51a2a64104d@o4g2000pbc.googlegroups.com>
 <82k445fu9n.fsf@stephe-leake.org> <jgfjc4$u4b$1@munin.nbi.dk>
 <MPG.29972ec7befb6ae9989682@news.zen.co.uk> <jgl70g$l9i$1@munin.nbi.dk>
 <MPG.299868e7ebbd43b1989683@news.zen.co.uk>
 <wccsjipfhlb.fsf@shell01.TheWorld.com>
 <MPG.2998d4eb6fbafe1a989684@news.zen.co.uk>
 <wccliohots1.fsf@shell01.TheWorld.com>
Reply-To: phil.jpthornley@gmail.com
MIME-Version: 1.0
User-Agent: MicroPlanet-Gravity/3.0.4
Organization: Zen Internet
NNTP-Posting-Host: c7edde12.news.zen.co.uk
X-Trace: 
 DXC=Xh4HCF?ko>PXHnR5[[clC[YjZGX^207P[`<MJMoM3PF]5Wf1?fiP5Y[6JNOYoB;SJ^I4^kRRZ1hN_CVdLP6@6@DT
X-Complaints-To: abuse@zen.co.uk
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Date: 2012-02-05T23:09:02+00:00
List-Id: <comp.lang.ada>

In article <wccliohots1.fsf@shell01.TheWorld.com>, 
bobduff@shell01.TheWorld.com says...
> 
> Phil Thornley <phil.jpthornley@gmail.com> writes:
> 
> > In article <wccsjipfhlb.fsf@shell01.TheWorld.com>, 
> > 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.
> 

Proofs don't really know anything about variables, only values. If a 
particular variable can take multiple values along a single execution 
path then either those values are defined by their expressions (which 
therefore replace the variable in the verification conditions) or if the 
expressions aren't known (usually because the variable is exported by 
one or more procedures) then the values are given different names, x__1, 
x__2, ...

Phil