Output contract's arguements

[PauloPinto]

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