Design by Contract != Runtime Assertion

[bearophile]

Walter:

> Most cases? I see it does some easy ones, but I'm skeptical it goes much beyond 
> that. It fails on this one:
> 
> class Example {
>    int x;
> 
>    void Inc(int y)
>            ensures (x & 1) == 0;
>    {
>      x += x;
>    }
> }

> This defeats the entire purpose of polymorphism. It doesn't make sense for Spec# 
> to be a polymorphic language if they're going to defeat it like this. It shows a 
> fundamental misunderstanding of polymorphism.

At the moment I have nothing more to add on this, thank you for your good answers. You and other people here have taught me tons of things :-)

Bye,
bearophile