Re: Preventing type extensions

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

On 9/23/10 10:49 PM, Dmitry A. Kazakov wrote:
> On Thu, 23 Sep 2010 21:00:01 +0100, Simon Wright wrote:
>
>> "Dmitry A. Kazakov"<mailbox@dmitry-kazakov.de>  writes:
>>
>>> Gosh, it was no more than just this: if horse is an animal that does
>>> not imply they are interchangeable. Compare: "all horses have hoofs"
>>> and "all animals have hoofs."
>>
>> I don't see your point.
>
> It was: the type /horse/ is not the type /animal/. That is not because of
> Ada's choice to keep them apart, it is because they are behaviorally
> (semantically) different.
>
>> You could make a near-infinity of operations on Animal like has-hooves,
>> has-tentacles etc but that would be silly. The only ops that make sense
>> at the Animal level are ones shared by all animals.
>
> All primitive operations are already shared, if it were only about type
> checks there would be nothing to discuss. Ada checks types.
>
> Beyond nominal checks, comparing two related types like horse and animal
> one considers substitutability. S is substitutable for T when any predicate
> P(T) remains true after substitution S for T. LSP subtype as defined by
> Liskov&  Wang

Wing, Jeanette M.

> are those maintaining substitutability. (All possible
> predicates exhaustively determine what in OO is called behavior. This is
> why Liskov&  Wang named it "behavioral notion of subtype.") My example
> illustrated existence of predicates turning false. Thus horse is not animal
> and animal is not horse (yet *a* horse is *an* animal). It is a tautology:
> a subset which is the whole set is not the whole set.

[Just trying to follow.]

"Subtype Requirement: Let Φ(x) be a property provable about objects
x of type T. Then Φ(y) should be true for objects y of type S where
S is a subtype of T."

(Where "property" is defined a little later.)

The authors emphasize that while Stack and Queue may share operations,
this type checked sharing of operations is not enough.
It does not guarantee that the programs will work the same way if
either is used, and likely not as expected. Not working correctly.

"Properties of an object's behavior" refers to states and
to sequences of states, as effected by prim ops:

Invariants:
   P(state) = True for all states.

History properties:
    P(state_1, state_2) = True for pairs of states.

I think that in your example, Horse (S) is not a subtype of Animal (T),
since Has-Hooves(x) cannot be proved for any x of type Animal.
A Horse object can substitute an Animal object IFF all prim ops
of Horse, including "extra methods", can all be expressed in terms
of Animal's prim ops *and* respecting the conditions placed on
the objects states and state sequences.  The programs must behave
the same, for Animals and Horses.
(That's how I have understood the model so far.)
Correct?

That is, when I assign an object of type Horse to a variable
of type Animal, then what matters is that the Animal program still
behaves as would be correct for an Animal program. But not necessarily
for a Horse program:  The "apparent" type (L&W) of objects will be
Animal, a specific type in Ada, and neither aliasing nor objects being
used in a different context (view conversions in another partition, for
example) will produce a state not correct for Animals.
If the program behaves differently when I use a Horse object where
an Animalis expected, then Horse is not a behavioral subtype of Animal.
Correct?


So, up to here, nothing in Liskov & Wing's Subtype Requirement
(as quoted above) corresponds to Ada's Animal'Class. [Just to
make sure I get the words right.]
Correct?