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 anObjectDisposedExceptionwhen called on an instance ofFoothat 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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With