Output contract's arguements

[Joseph Rushton Wakeling]

On 19/09/13 16:39, H. S. Teoh wrote:
> At the very least, it would be nice to have access to x.old, as Eiffel
> allegedly allows, if we insist on letting x refer to the copy of the
> input value modified by the function body.

I absolutely agree that access to x.old is needed, but I don't see the value or 
purpose in excluding the final value of x from the out checks -- it's useful to 
be able to check those values, too.