The Visual Studio plugin and the dafny.exe command line both use the Dafny compiler to verify your code. However, that's not good enough for Ironclad, whose aim is to verify every assembly instruction that will execute on the system. So although the Dafny plugin and command-line tool are useful pre-build checks to see if your code is verifiable, passing either is no guarantee you'll satisfy DafnyCC, which is what the ultimate build process uses. Most of the time, it will, but here are some guidelines to get your code in shape to also pass DafnyCC.

Sequence-based invariants
Arrays in datatypes
Null arrays
Automatic induction
Calc hiding
Mathematical _forall lemmas
Conservative sequence trigger

Last edited Oct 15, 2014 at 12:10 AM by howell, version 1


No comments yet.