Question about unreachable program point

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

Hi,

Here is a program that has unreachable program point:

http://rise4fun.com/Dafny/pLVy

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?