Output contract's arguements

[bearophile]

monarch_dodra:

> 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".
>
> In particular if/when we will have "contracts are 
> managed/compiled by caller", then that behavior is the only 
> behavior we will be able to do (AFAIK).
>
> Or is there something that explicitly states it works that way? 
> Should I file a bug report? ER?

This is an example of "leaky abstraction", caused by the D 
implementation of contracts.
What is the behavior of Ada and C# contracts on this?

Bye,
bearophile