Re: On pragma Precondition etc.

[Georg Bauhaus <rm.tsoh.plus-bug.bauhaus@maps.futureapps.de>]

Dmitry A. Kazakov wrote:

>> Any preconditions are those that you specify, of course.
>> They don't magically start to exist[*],
> 
> Of course they do. If there is no explicit precondition specified for an
> argument X of the type T, it still exists, and is:
> 
>    X in T [and true]

OK.  They usually say "silly argument" in DbC discussions.


> 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?



> [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.  The Precondition isn't checked
at runtime because the constraint violation happens earlier,
as this is Ada.


> 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 wrong with pragma Precondition?


>> 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.
(As I said, there might be variance problems because Ada subtypes are
superclasses considering only the set of values.
Writing Ada, you are always free to design variance problems
using 'Class parameters.  I don't see a reason why Ada-DbC cannot
enhance this situation.)



>> 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.)

Could you point to your definition of "contract"? It seems to
differ from what everyone around Design by Contract understands
it to be (and understands pragma Precondition as it is now).


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

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

Yes?

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

> [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?