Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

On 24.06.12 18:06, Dmitry A. Kazakov wrote:
> On Sun, 24 Jun 2012 16:59:55 +0200, Georg Bauhaus wrote:
>
>> On 23.06.12 13:01, Dmitry A. Kazakov wrote:
>>> Compare: a contract violation is an *unbounded ERROR*.
>>
>> Do you mean, I should imagine a contract violation that,
>> when checks are turned off, result in erroneous execution?
>
> The effect of contract violation is unbounded because not contracted.

The effect of a contract violation is part of the contract between
client and supplier, by definition, even when it appears to be rather
trivial:

When working under the rules of DbC, a violation that is detected by
the contract checking system must engage the exception mechanism.
This mechanism is supposed to entail a rescuing action, recursively,
or a bail out---and there is LRM 11.6, anyway.

So,

1. if X0 might violate the contract of ADT[*] Y, then X0, or some Xn
    on X0's behalf, must handle the effect of the violation,
    as outlined. There is a guarantee that every (efficiently decidable,
    let us say) violation is detected if (a) checks are on, or
    (b) the proof obligation has had the effect of showing that there
     is no violation, for all inputs.
  
2. Effects of exceptional situations may or may not be expressible
    at all, due to the nature of Ada exceptions that, unfortunately,
    cover both "exceptional situation" and "non-local transfer of
    control". In "exceptional situation", there may not be any form of
    control because this is what the word "exception" means in this
    case: the program can control all situations except those whose
    effects are not known when designing. We would be trying to handle
    Program_Error in advance.


> When you say that something behaves in a certain way under specified
> conditions, e.g. raises exception when out of range, that is the contract.
>
> 1. violation =>  nothing guaranteed
> 2. effect is bounded =>  these bounds are in the contract
>
> 1+2 = contract violation is necessarily *equivalent* to undefined behavior.
>
> What is so difficult about this?

It is a theory in a different universe of notions.


__
[*] A contract as in Design by Contract applies to ADTs only, somewhat like
the full set of different aspects is made for ADTs in Ada 2012.