Prior to your response, I was rechecking "Inheritance Model". My issue arises from section 10 of that document. For the first time using Rel/Tutorial D, I feel I disagree with a design point of the language, rather than merely failing to understand the syntax. As a consequence I will raise this issue on the TTM list (or at least point out the existence of this thread). However, there are still other points arising from this example, spelled out below.
I believe that section 10 of the document describes a necessary, but not sufficient definition of subtyping by specialisation constraint. The missing piece is an amendment so that it reads:
that a value shall be of type T' if and only if it is of type T, it satisfies constraint SC, and is defined (or assigned) as being of type T' or one of its subtypes.
This would permit overlapping constraints, and would prohibit a value changing type just because it happens to meet a constraint on one of its subtypes. I believe the example we have been discussing shows a justification for this change. I set out below section 10 together with my proposed amendment.
While making this suggestion, I do want to check that I am not missing a capability of the language that would enable me to define data types with overlapping constraints without generating an effective change of type from supertype to subtype if it happens that constraints defined elsewhere are met. In addition to the major design point about type inheritance, there is a minor syntactical query hidden in my example. Why does
Code: Select all
greater_than(unbounded_integer("1"),unbounded_integer("1"))
not return a boolean value of false?
Section 10
Let T be a regular type (see IM Prescription 20) and hence, necessarily, a scalar type, and let T' be a nonempty immediate subtype of T. Then the definition of T' shall specify a specialization constraint SC, formulated in terms of T, such that a value shall be of type T' if and only if it is of type T and it satisfies constraint SC. ...
Section 10 amended
Let T be a regular type (see IM Prescription 20) and hence, necessarily, a scalar type, and let T' be a nonempty immediate subtype of T. Then the definition of T' shall specify a specialization constraint SC, formulated in terms of T, such that a value shall be of type T' if and only if it is of type T, it satisfies constraint SC, and is defined (or assigned) as being of type T' or one of its subtypes. ...