[nem-en] Advanced contracts handling and Mono

[Michal Moskal]

On 7/14/06, Arthur Peters <amp at singingwizard.org> wrote:
> I just noticed that there is an advanced version of the contracts macros
> that supports compile-time validation (in tools/contracts). That is very
> cool, but I cannot use it because I am Linux only and it requires the MS
> spec# code (and a few other things it seems).
>
> Are there plans to port this to the Mono world? If so when will it
> happen? If not, why not?

It requires boogie verification condition generator that probably
won't run under mono. Even if it does run, I'm not sure license allows
using it on non-MS platform (it's a project by MS Research).

> Also a random question about the code: Are "ensures" and "invariant"s
> inherited by derived classes (aka automatically added to overriding
> methods)? I would want this because it enforces the principle that
> derived classes can be treated as the base class.

I think so. However I'm not sure. Maybe Wojtek will be able to help.

-- 
   Michał