Question about unreachable program point

Nov 4, 2012 at 5:27 AM
Edited Nov 4, 2012 at 5:28 AM


Here is a program that has unreachable program point:

Dafny complains about the post-condition at the point which is unreachable

I use this ghost method to return the index of an element.

As a workaround, should I just omit the implementation of it instead?