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=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!gandalf.srv.welterde.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: {Pre,Post}conditions and side effects
Date: Tue, 12 May 2015 17:08:46 -0500
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <mittlf$v1l$1@loke.gir.dk>
References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com>
 <AnYlw.957256$Rp.242412@fx23.iad>
 <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com>
 <wccoaqucn51.fsf@shell01.TheWorld.com>
 <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com>
 <alpine.CYG.2.11.1412231747100.4196@WIL414CHAPIN.vtc.vsc.edu>
 <wccegrpq2om.fsf@shell01.TheWorld.com>
 <87tww5296f.fsf@adaheads.sparre-andersen.dk> <871tj9dp5b.fsf@theworld.com>
 <ce4af31e-d491-479f-a5b3-0b3eedea2a68@googlegroups.com>
 <midvq5$2u3$1@loke.gir.dk> <alpine.DEB.2.11.1505071103310.14859@debian>
 <migc9a$jp8$1@loke.gir.dk> <alpine.DEB.2.11.1505072052570.16448@debian>
 <mijen0$1hj$1@loke.gir.dk> <alpine.DEB.2.11.1505111113020.12062@debian>
 <mirjho$lqh$1@loke.gir.dk> <mis9kh$ief$1@dont-email.me>
NNTP-Posting-Host: rrsoftware.com
X-Trace: loke.gir.dk 1431468527 31797 24.196.82.226 (12 May 2015 22:08:47 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Tue, 12 May 2015 22:08:47 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Response
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157
Xref: news.eternal-september.org comp.lang.ada:25854
Date: 2015-05-12T17:08:46-05:00
List-Id: <comp.lang.ada>

"Georg Bauhaus" <bauhaus@futureapps.invalid> wrote in message 
news:mis9kh$ief$1@dont-email.me...
> On 12.05.15 03:03, Randy Brukardt wrote:
>> Consider just the interesting properties of a Vector container. The 
>> length,
>> capacity, and tampering state all immediately come to mind, and most
>> routines change none of them. How to communicate that?
>
> By your own words, wouldn't you just ask for a predicate
> that expresses all of that? Something like
>
>   Is_Mostly_Unchanged_A (Vector)
>
> in the positions you find adequate?

That would work, but you'd need a number of them (for all of existent 
combinations of unchanged). But it does nothing for the readability problem 
of cluttering everything with that.

Humm, actually it doesn't work (at least not as you wrote it), because 'Old 
can only be written in a postcondition. (Else the lifetime issues become 
maddening.) You could write:

Is_Mostly_Unchange_A (Vector, Vector'Old)

but that is a lot more expensive than the original, as here the entire 
vector is getting copied for the check, rather than just a bunch of simple 
properties.

In any case, I've been mostly focusing on the precondition/predicate part of 
the proof. The postcondition/type_invariant part is a rather different 
kettle of fish.

                                        Randy.