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
