Re: Operation can be dispatching in only one type

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

On Mon, 7 Dec 2009 18:19:11 -0600, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:1gcigitaii0u0.1psu2vj52e66g$.dlg@40tude.net...
>> On Fri, 4 Dec 2009 20:45:19 -0600, Randy Brukardt wrote:
>>
>>> Writing in Ada 2012 as proposed today
>>> (and that might change before it gets standardized):
>>>
>>>      procedure Do_Something (Window : Claw.Basic_Window_Type; ...)
>>>              with Pre => Is_Valid (Window);
>>
>> Why not to allow such constraints for subtypes? E.g.
>>
>>   subtype Valid_Window_Type is Window_Type when Is_Valid;
>>
>> then simply:
>>
>>   procedure Do_Something (Window : Valid_Window_Type; ...)
> 
> That's also under consideration, but there are some problems with it. One 
> problem is that such types are very confusing in array indexes/slices (do 
> the values all participate or just the ones that pass the predicate?)

Only ones of the subtype, obviously. But the problem is same as with the
index sliding: when two subsets of the index are equivalent, either
nominally (when elements are same) or structurally (when the number of
elements is same + maybe other conditions). Structural equivalence might
appear convenient, but it is always a source of confusion.

> are a couple of others as well.
> 
> Another issue is that not all preconditions/postconditions can be written 
> this way. For one thing, a precondition can depend on multiple parameters at 
> once. Another issues is that the entry condition and exit conditions may be 
> different for a parameter. For instance, from Claw:
> 
>      procedure Create (Window : Basic_Window_Type; ...)
>          with Pre   => not Is_Valid (Window),
>                  Post => Is_Valid (Window);

Mutating [sub]type? That looks like a case for a constructor to me (an old
discussion).

> So subtypes cannot completely replace pre and post conditions, but they can 
> be a complement to them.

Absolutely.

However I consider it differently. In my view pre-/postconditions and
invariants should be static, used strictly for program correctness proofs.
Subtypes should complement them for dynamic run-time checks (recoverable
faults).

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