Re: {Pre,Post}conditions and side effects

[Robert A Duff <bobduff@shell01.TheWorld.com>]

Jean François Martinez <darkquark99@gmail.com> writes:

> On Tuesday, December 23, 2014 6:05:33 PM UTC+1, Robert A Duff wrote:
>
>> I don't agree with that.  It sometimes makes sense for pre/post to
>> check values of global variables.  Probably not often -- after all,
>> it's not often that you should have global variables in the first place.
>> But surely if the job of a procedure is to update some global,
>> it makes sense to have a postcondition ensuring that it did so
>> correctly.
>
> That was clumsy (I was in a hurry) wording of my part.  Should have
> been "a pre/postconsition/invariant" usually don't involve redoing the
> whole calculation but just checking values of "data entities" both in
> the absolute and relativly to one another.  Most of the tilme you
> don't write pre/postonditions/invariants involving (with functions
> cvalled) tens of thousands of programming lines and gazillions of CPU
> cycles

Yes, I agree.  The best assertions are much shorter than the executable
code.  For example:

    function F return Integer is (123) with Post => F'Result = 123;

If you manage to prove that postcondition, you haven't accomplished
much.  Likewise, if 123 were replaced (in both places) with 1000 lines
of code, you still haven't accomplished much -- it's just as likely
there's a bug in the postcondition as in the function itself, especially
if the postcondition duplicates the function, which I assume is what you
meant by "redoing the whole calculation" above.

But if the function is long, but its postcondition is short, then
proving the postcondition is a big win.  The goal is to somehow
characterize what the function is supposed to do more concisely than the
code that does it.  Not always easy.

- Bob