Re: Seeking for papers about tagged types vs access to subprograms

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On 11 May 2013 11:49:12 GMT, Georg Bauhaus wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:
> 
>> The condition is moved to the post-condition. E.g.
>> 
>> # require X >= 0.0
>>    function sqrt (X : Float) return Float;
>> # ensure sqrt (X)**2 = X
>> 
>> is replaced with
>> 
>> # require true
>>    function sqrt (X : Float) return Float;
>> # ensure sqrt (X)**2 = X or else Constraint_Error raised
> 
> So sqrt tests X for being non-negative and raises C_E otherwise?
> Can the test be turned off?

It is not test, it is a behavior. However if sqrt were inlined, at least
partially, one branch of "if" could be removed if its condition proved
static.

> # require true
>   procedure increase_pressure (P : in out Pot; X : Float);
> # ensure pressure (P) = X * pressure (P'old) or else Kaboom raised
> 
> So where goes the precondition of the second kind mentioned
> earlier, for calls, the one that is needed for correctness of the program?

Is it a physical system you are talking about? In that case it does not
work this way. You have a hardware in the [control] loop (HIL). E.g. a
valve, a boiler, whatever. You set the valve using an actuator, you control
its position using position sensors, you control pressure using pressure
sensors, you control things using indirect measures, e.g. of the
temperature etc. There is a model of the system according to which you act
and react. It is very different from digital deterministic systems where
cause and effect are tied to the point of being equivalent.

> I take it that the former kind of precondition prevents Kaboom in the
> system?

By not raising it. So long the model is adequate [as estimated though the
sensors] you don't raise anything. When the model is no more adequate you
drive the system into a definite state as specified by the requirements,
e.g. by doing an emergency shutdown. This procedure may be implemented
using exceptions. In some cases definite state is achieved by self
destruction (see Ariane).

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de