Design by Contract: Can we express Stack FILO property with contract?

It seems that design by contract has limit to express specification. For example, i tried to express Stack FILO property with contract, but didn't get an idea. Anybody can help?

I think the root cause is that precondition/postcondition/invariant are assertations without side effects. It leads to the checking of开发者_Go百科 FILO property which is a kind of side effects not easy even possible.

That's true, design by contract has limited functionality. They are not panacea. Because if they were then the IT industry would throw out unit-testing, code reviews etc.

I suggest you to write simple unit-test for this case rather than crack your head by implementing a contract (which even may be unimplementable).