WeakBehavioralSubtyping

Weak Behavioral Subtyping

The JML Reference Manual describes a concept called weak behavioral subtyping, which is from Kishore Dhara's Ph.D. dissertation. This is supported in JML by the keyword weakly, which may be used to indicate that a type is only a weak behavioral subtype of some other type. The semantics are that history constraints are not inherited by weak behavioral subtypes.

The main problem with this is that to be sound, a notion of weak behavioral subtyping must be accompanied by restrictions on references, which must obey a viewpoint restriction, meaning that each object can only be referred to by references of at most one static type. And JML has no way to enforce such a viewpoint restriction.

Additionally, weak behavioral subtyping is a complication that is seldom if ever used or mentioned in JML papers or examples. As such we could easily simplify the language by omitting it.

There being no objections, the feature of weak behavioral subtyping, and the weakly keyword are hereby dropped.