The noCheating flag

Mar 1, 2013 at 10:16 PM
Hi Rustan,

My version of dafny flags a compilation error if the program contains "assume" statements, but does not complain if it contains ghost methods with no bodies (which amounts to the same thing).

Similarly, /noCheating:1 does not complain about miraculous ghost methods.

I wonder whether it would be consistent to organise things so that

(1) Dafny -will- compile programs with assume statements (simply ignoring them, as it does miraculous ghost methods). Maybe someone wants to test their program before it's fully proved?

(2) Dafny /noCheating:1 -won't- allow miraculous ghost methods. A good use of noCheating would be to make sure that there remain absolutely no holes (unproved lemmas) of any kind, ie that you really are finished.

Thanks!