Re: {Pre,Post}conditions and side effects

["Randy Brukardt" <randy@rrsoftware.com>]

"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.