On 19/09/13 14:04, Artur Skawina wrote:
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...
That seems to be a theoretical ideal that doesn't acknowledge the practical benefits of being able to check final values of local function variables on exit.
I'm not sure that it can really be described as leaking given how contracts are apparently implemented in a practical sense.
