Re: On pragma Precondition etc.

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

On Fri, 01 Aug 2008 01:06:42 +0200, Georg Bauhaus wrote:

> Dmitry A. Kazakov wrote:
> 
>> when you hang some contracted constraints on the
>> parameters of a subprogram, you implicitly define a set of derived types
>> constrained to that.
> 
> I could define artificial types so that Boolean expressions
> could become primitive Boolean functions of that artificial type.
> But I don't. What's the big gain?

To have it typed. When you just sow arbitrary conditions here and there,
you cannot reuse or reason about them generally. It is uninteresting and
there is pragma Assert for that. (possibility #1)

>> [a liberal explanation of LSP skipped]
>> 
>>> Seen in this light,  range 1 ... 500 takes away values
>>> from Integer'range.  (Not surprisingly, since it is a constraint.)
>>>
>>>     subtype My_Integer is Integer range 1 .. 500;
>>>
>>>     overriding
>>>     procedure Bar(Item: My_Whatever; Num: My_Integer);
>>>
>>> With or without DbC, it seems reasonable to me to expect
>>> that Bar fails when it gets an argument for Num outside
>>> range 1 .. 500.  Say it fails with a Constraint_Error.
>> 
>> No, it fails at compile time, provided, 1 .. 500 goes into the contract,
>> because the result is not LSP-conform.
> 
> An Ada compiler will compile the code,
> 
>   function Foo(X: My_Integer);
>   pragma Precondition(X <= 500);
>
>  Bound := 501;
>  ...
>  Foo(Bound);
>
> My compiler may warn that the program will raise a Constraint_Error,
> but the code is legal.

See, it is not a contract. If it were a contract you would not be able to
pass Bound to Foo due to a contract violation. pragma Precondition did not
change the contract of Foo.

>> But the question was different. It was about composition of conditions in
>> presence of tuples of parameters. You consider each parameter and its
>> contracted constraints independently, this is wrong.
> 
> In what frame of reference is it wrong to express a boolean relation
> between parameters?

What is the semantics of the relation? #1?

> What is wrong with pragma Precondition?

1. Untyped, not reusable, cannot handle polymorphism, non-composable (and
other more or less equivalent statements)

2. Changes the program semantics (in general case cannot be ignored, and
undecidable if it could be)

3. Statically uncheckable

>>> This exceptional behavior is already illustrating why the DbC
>>> idea of having a 'Constraint on a type makes sense.  It is
>>> already working for subtypes now.
>> 
>> Wrong. Ada constraints are not contracts.
> 
> In the sense of Design by Contract Ada constraints add to a contract,
> even though it is a trivial one like X in My_Integer'range.

No, it adds nothing. When you create an Ada subtype the contract of the
result is not changed. It is still "X in T, and Constraint_Error may be
propagated."

> (As I said, there might be variance problems because Ada subtypes are
> superclasses considering only the set of values.

Hmm, I don't know what you mean under "superclasse" in this context.

>>> Many shrug when they
>>> are more busy with the practical benefits of DbC.
>> 
>> I don't buy it. Practice unsupported by a sound theory is shamanism.
> 
> DbC is about programming, in addition to being about programs.
> Is there a sound theory of programming? We do have some sound
> theories concerned with aspects of programs.  These aspects
> can be extracted from just the program. Assertion checking
> in the Design(!) by Contract sense never looses sight of the process
> of programming.  (Neither does the word "pragma" as in
> pragma Precondition.)

I don't get the point. Is it that assertions and preconditions are merely
comments for a well-disposed reader?

Under "sound theory" I understand at least a comprehensible definition of
the semantics of conditions. Is

   pragma Precondition (X);

intended to be an abbreviation for horribly long:

   if not X then
      raise Assert_Error;
   end if;

That's one possible interpretation (#1). I don't think people would enjoy
it much. But it is still better than vague references to "practical
benefits." If you want to move beyond #1 you will face problems.

> Could you point to your definition of "contract"?

A restriction put on multiple parties (like callee/caller) identically true
in a correct program.

>> ------
>> BTW, we could drop the idea of making conditions [<del>]contracted[</del>]
> <ins>a statically verifiable property of some hypothetic type
> system</ins>.

Sure (I read "hypothetic" as "strongly typed")

>> Instead of
>> that, we would consider constraints in the sense of Ada subtypes.
> 
> Yes?

Yes. It would allow interesting so things. For example, one could define
subtypes of odd numbers, integers without zero, dimensioned values, etc.

>> In that case it would be [<del>]all[</del>] dynamic, run-time,
> <ins>as well as food for the compiler</ins>.

Rather useless food. The compiler may not reject the program because
constraints would not influence the program semantics. [Unless exceptions
would become contracted.]

>> [Contracted constraints are more like SPARK model] But in any case the
>> problem would remain.  We would have to introduce anonymous subtypes
>> of tuples of [sub]types.
> 
> Checking a condition means calling a well defined functions at
> well defined times.

(??)

>> In both cases we need a [sub]type to associate the
>> constraint with.
> 
> Why?

Because there is no other vehicle. Constraints are put on subtypes. If you
want to put constraints on sets of, which is implied by mixing multiple
parameters in one expression, then you need subtypes of tuples of types.

Of course, if you don't consider it as #1 above.

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