A question about DbC

[Jonathan M Davis]

On Saturday 09 October 2010 06:02:52 bearophile wrote:
> Jonathan M Davis:
> > What's odder is that the invariant is run after the
> > precondition. That shouldn't be necessary, since any changes to the
> > object would have been verifed after the last time that a public member
> > function was called.
> 
> They may contain different tests.

True, but assuming that there is no way to access the state of the object except 
through its public functions, then running the invariant before executing a 
public function is pointless, because it was already run after the last public 
function was called, and there's no way that the state of the object could have 
changed in the interim. However, given that returned references and pointers as 
well as public member variables would allow you to alter an object outside of 
its public functions, the object's state could have changed between its last 
public function call and the new public function call, so that's probably why 
the invariant is run before the public function is. However, if the state 
couldn't have changed since the last public function call, the running the 
invariant before the function call is pointless.

- Jonathan M Davis