Invariant and pre/post-conditions order

[Manfred Nowak]

Walter Bright wrote:

> I recently fixed the specs to define the sequence.

Then the Status Quo holds. One more remark:

if the intention still is, that contracts are to be seen as an 
executable description of at least parts of the design, then the 
current specification of the language does not give any control over 
those contracts to the designers.

This is because the coder can easily change the contracts and then the 
designer would have a hard time to find that modifications.

This could be changed for eaxmple by compiling the contracts into a 
separate library but seems not to be supported.

Are there other ways to garantie, that the code the coder delivers to 
the designer indeed fulfills the requirements the designer gave before 
handing out the job?