Refining a contract
-- state responsibilities and obligations
invariance
-- respect the invariants of the base class
methods
-- services may be added or refined
Refining a method
-- like improving a business contract
class C : public P { virtual void m(); }
pre(
m_C
)
>=
pre(
m_P
)
post(
m_C
)
<=
post(
m_P
)
slide
:
Contracts and inheritance
