Re: {Pre,Post}conditions and side effects

[Georg Bauhaus <bauhaus@futureapps.invalid>]

On 25.04.15 14:08, vincent.diemunsch@gmail.com wrote:
> But what Ada and SPARK 2014 are doing is "design by contract", as Bertrand Meyer
> called it. This makes a confusion between a precondition and a runtime test.

Actually, Meyer insists that contracts have an associated
notion, that of proof obligation. And the description of DbC
is declaring quite openly that not needing to perform run-time
tests (e.g. defensive programming) is a design goal.

What you get in the lesser (than some fancy ideal) situation is
summarized in a table of OOSC2, §11.6 (coincidence? ;-), for a stack:

   Put        OBLIGATIONS          BENEFITS

Client    satisfy Pre=>...        from Post=>...

          Only call Put(X) on     Get stack updated: not
          a non-full stack.       Empty, X on top, Item yields
                                  X, Count increased by 1.

Supplier  satisfy Post=>...        from Pre=>...

          Update stack reprsntn   Simpler processing thanks
          to have X on top (Item  to the assumption that
          yields X), Count        stack is not full.
          increased by 1, not
          Empty.


Looking at SPARK 2014, it seems to not have changed earlier SPARK
WRT being a tool for analysis before run-time.

Ada, OTOH, looks like becoming a programming language facilitating
either type of checking, as before, but more extensively and more
formally, and more of it to write for the programmer.