On Wed, 20 Jun 2012 08:39:50 -0500, Nasser M. Abbasi wrote:
> But, and here is the problem, when I turn off assertions, I am
> now left with the push() function with no check at all for
> the case of the stack is full.
> So, what is one to do? use pre/post AND also add
> an extra check for full stack in the code as before?
> does not make sense.
This is what constitutes the core inconsistency about dynamic
pre-/post-conditions. If they #1 implement behavior (e.g the stack contract
to raise something when full), then they cannot be suppressed and do not
describe the contract. If they do describe the contract #2, they may not
implement it and thus shall have no run-time effect.
> They seem to definitely be something good to have.
Not everything is what it seems...
Dmitry A. Kazakov