Re: Ada Interfaces and the Liskov Substitution Principle

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

Markus E Leypold wrote:
> 
>> I bet that as soon as someone popularizes a mathematical model

>> If I had the money, I'd put up a challange that triggers some
>> programming oriented model research

> Somehow you seem to think, we can just do away with the models, if we
> just approach it right.

No. We might profit from mathematical models that are even better
because they better reflect what programming staff needs. (Reminds me of
the intent that has led to Ada.)

Perhaps this was misleading:
>> Until then, only this or that kind of variance is allowed to exist,
>> for either mathematical or problem domain reasons, because the
>> other solution cannot but create an unmaintainable mess...

WRT variance, one of Meyer's examples is the allocation of boys and
girls to dormitories.(*)
  Boys and girls are two sexes of the human kind, hence Boy and
Girl are derived from the type Human. Girls' dormitories
and boys' dormitories are two derived types of domitories.
There is a procedure for each Human object, say Person,

  Person.Accomodate(dorm => ?Dormitory?);

that will place a person in a dormitory, such that girls sleep
in the girls' dormitory and boys sleep in the boys' dormitory.
  Shall we have a procedure for boys (or girls) that just takes
a person of the respective sex and places the person in a
dormitory'class?

  procedure Accomodate(who: Boy; dorm: Dormitory'class);

(Of course, the "moral rule" depends on who you ask, but this example
presumes gender segregation in any sexual sense.)

There is a subsection in the corresponding section (OOSC2, �17) entitled
"Polymorphic perversity". It alludes to the consequences of
different "co/contravariance policies", speaking about a procedure that
expresses "sharing a room".

  type Boy is new Human with private;
  overriding
  procedure Share(self: in out Boy; other: in out Boy);

This definition meets the requirement that a boy and a girl shall not
share a room.
OTOH, there are also technical arguments in favor of defining a
procedure that doesn't vary in the same "direction" as the type,
thus

  type Boy is new Human with private;
  overriding
  procedure Share(self: in out Boy; other: in out Human'class);

Which co/contravariance policy is right? And therefore, can we
decide which model is the right one if all that we can say about a
model is that it is mathematically sound in some sense?
  Of course it is, but soundness is very likely just a necessary
precondition. Whether a model is sufficient, and more precisely,
in which cases it is sufficient, these are the more interesting
questions (to me, at least).

(*) (There are certainly other solutions that do not
involve inheritance, but this is the illustration given. I'm varying it
slightly.)