Invariants on interface contracts
- Is it valid to create an invariant method in a contract class for an interface? Presumably the rewriter would have to create the equivalent method in the implementation class.This doesn't seem to be supported right now - is it a deliberate omission (which I should feel free to document :) or is it likely to change?Jon
Web site: http://www.pobox.com/~skeet Blog: http://www.msmvps.com/jon.skeet
All Replies
- I don't think this is a good idea. An invariant is an internal implementation detail which doesn't belong on an interface.
Can you give an example of a condition which should be an interface invariant? I can't think of any good ones. - Say I have a property on an interface that defiens the price on a stock. It can not be negative, and I must reject any negative prices. I add the precondition on the interface. But since I don't have the underlaying field, I cannot add invariants on this field.
Now, in the constructor for the class that implements the interface, when I set the value for the underlying field, I loose this implementation detail, and set the field to a witness value (-1), that violates the precondtion.
Furthermore, if this class is serializable, I'm open to a host of bugs that derive from this tini-tiny detail that interfaces cannot add invariants.
makes sense? - I would implement that as a Price property which had a precondition on the setter that the value be non-negative and a postcondition on the getter that the result be non-negative.
Any condition involving one member of the interface can be implemented as preconditions and postconditions on that member. I think every possible invariant, as seen from the outside, can be implemented as preconditions and postconditions on the interface. - I don't have any examples, and I agree it may well not be a good idea. I'm really just checking that it's not allowed, and isn't likely to be in the future :)
Web site: http://www.pobox.com/~skeet Blog: http://www.msmvps.com/jon.skeet
