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...

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de