Output contract's arguements

[Artur Skawina]

On 09/19/13 15:03, PauloPinto wrote:
> On Thursday, 19 September 2013 at 12:04:34 UTC, Artur Skawina wrote:
>> On 09/19/13 13:11, Peter Alexander wrote:
>>> On Thursday, 19 September 2013 at 11:07:07 UTC, Artur Skawina wrote:
>>>> On 09/19/13 12:58, Peter Alexander wrote:
>>>>> On Thursday, 19 September 2013 at 10:44:32 UTC, monarch_dodra wrote:
>>>>>> On Thursday, 19 September 2013 at 10:38:37 UTC, Joseph Rushton Wakeling wrote:
>>>>>>> On 18/09/13 14:11, monarch_dodra wrote:
>>>>>>>> IMO, this is wrong. When calling a function with an out contract, the arguments
>>>>>>>> should *also* be passed to the out contract directly. "out" should not be
>>>>>>>> expected to run on the body's "sloppy seconds".
>>>>>>>
>>>>>>> I'm not sure I understand your objection here.  As I understood it the whole point of an "out" contract was to check the state of everything _after the function has exited_.
>>>>>>
>>>>>> Exactly.
>>>>>>
>>>>>> If the function has already exited, then why is the state of he arguments modified? I though pass by value meant that the function operated on its own copy?
>>>>>
>>>>> What exactly would you like this to do? v only exists inside the body of the function. There is no v after the function exits. If you check v in the output contract then you are checking the final value of v.
>>>>
>>>> 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.
>>
>> A contract only describes the /external/ interface (inputs, outputs
>> and visible state).
>> It makes no sense for it to depend on any local private variable of a
>> method; 'assert's in the function body can be used to verify the
>> implementation.
>> Leaking the internal state into the contracts has consequences, such as
>> making it much harder to use the same executable/library/archive for both
>> debug and contract-less builds (well, w/o duplicating all the code,
>> instead of reusing the bodies). Being able to easily check the contracts
>> at the exe<>dll boundary is important; if this requires using a different
>> library binary or causes massive bloat then this feature simply won't be
>> used much...
> 
> 
> Sorry but this is not like that.
> 
> Contracts also make use of invariants for the internal state of the object.
> 
> This is exactly what out conditions are suppose to validate.
> 
> - The internal invariants are still valid on function's exit
> - The returned value and parameters passed by reference have the expected values
> 
> At least if D is supposed to follow what Design by Contract means in languages that already provide it, specially Eiffel which is the language that gave birth to these ideas.

While I can see some value in verifying /internal/ state (and not just
"visible" like i said above), it should be *persistent* state, ie not
just something completely local to a method, that ceases to exist on
exit. Asserts are there for checking local assumptions.

The practical aspect is -- iff you don't leak implementation details
then contracts in a dynamically loaded library can be handled like this:
compile the body of a function and its in/out/invariants as separate
functions, plus emit an extra one which calls the contract code in 
addition to the original function. Now you can call, say, f() to execute
the overhead-less body, or call f_with_contracts() to run the extra checks
too. The cost of enabling contracts is small; just a slightly larger
binary, no runtime penalty, unless requested. And, as dynamic linking
already implies a level of indirection, the choice of running with or
without checking the contracts can even be done at *runtime*.
This is probably *the* most important use-case of contracts in a language
like D; if this can't be handled effciently, then D could just drop all
support for contracts.

Note that in the above scenario the compiler would need a three-way switch
"contracts = (None|Externally_visible|All). The 'All' case would cause all
emitted code to call the contracts - you'd use it while working on and
testing eg a library. Then, when you release it, you build it with
'contracts=Externally_visible', which will emit the contract funcs, but
will never actually /call/ them. This means that some /internal/ contracts
are not run, but that's ok, as in return you receive *zero* perf overhead.
You can now ship the dll as-is, and /the user/ gets to choose if he wants
to enable contract-checking. No need to worry about linking with right
version of the library; the support is always there. And the cost is
just a slightly larger file, that goes away if you recompile the lib with
'contracts=None' (or use a tool to strip the extra code).

Keeping the mistake, that exposing the local args was, not only makes no
sense, but would prevent implementing saner contract support.

artur