This is a highly general thought, but let's use C# in this example.
Given that
Foo
, i.e., it implements IDisposable
.Foo
has a boolean flag disposed
that is false until Dispose
is called, after which it's true.Foo
throws ObjectDisposedException
if disposed
is true when they are called.Does this statement
Any method of
Foo
, exceptDispose
, will throw anObjectDisposedException
when called on an instance ofFoo
that has been disposed.
describe an invariant of Foo
?
No.
This is a set of rules common to all the methods of the class. Invariants are not rules for methods.
Design by Contract comprises defining the following parts of a contract:
What you are describing are method postconditions. They belong to the contract of each function (which is of course part of the contract of the class), but not to the class invariant.