On Thursday, 19 September 2013 at 11:18:54 UTC, monarch_dodra
wrote:
On Thursday, 19 September 2013 at 11:11:58 UTC, Peter Alexander
wrote:
On Thursday, 19 September 2013 at 11:07:07 UTC, Artur Skawina
That "final value of v" is not part of any contract, it's
just a private
local.
I repeat my question then: what would you want this to do? As
you say, v is a local copy, it cannot be part of a contract --
it cannot affect anything the client code sees.
I'd like the out contract to operate on its own copies of the
function's arguments.
These could either be passed by the implementation of the body,
prior to starting proper, or by the caller, passing the same
arguments to both the contract and the function. That'd be
dependent on the implementation.
Using the Eiffel standard as reference, chapter 8.9, the daddy of
design by contract
http://www.ecma-international.org/publications/standards/Ecma-367.htm
Given a parameter x, on a postcondition it refers to the local
value on function's exit. To refer to the original value on entry
it needs to be prefixed with the keyword old.
--
Paulo
