#137 RAC skips code specification cases

[Clyde D. Ruby]

Currently, the RAC does not handle specification cases
modified by the code keyword because such cases do
not have the same inheritance semantics as other
specification cases. In particular, code contracts are not
inherited by the subclass when the method is overridden.
That is, these code specification cases specify
properties specific to the implementation in which they
appear and thus are not inherited when the method is
overridden.
The RAC also needs to handle the \same predicate in
requires clauses. A \same means that all the clauses in
the body of this specification case apply to all other
specification cases that do not have a "requires \same"
clause. Thus \same means the disjunction of the
preconditions in all the other specification cases.

[Gary T. Leavens]

Logged In: YES
user_id=633675

See also Feature Request 1368585.