Is there some way to run Z3 over hand-made verification conditions?

Oct 30, 2013 at 12:04 PM
Hi,
I'm preparing an undergraduate course on "Formal Methods for Software Development". I would like to show the students a little of how Dafny works. To this end, I would like to run Z3 over handmade verification conditions to show the Z3-answer. Is there some way to do that?
Developer
Oct 30, 2013 at 1:28 PM
Hi,

sure, Z3 accepts input in the SMT-LIB format (see http://rise4fun.com/z3 for some examples and http://rise4fun.com/z3/tutorial for a tutorial). You could also check out the /proverLog command line option in Dafny to see what the VCs look like that Dafny/Boogie produce.

Best regards,

Valentin
Oct 30, 2013 at 2:39 PM
Hi Valentin,

Could you tell me where could I find information about "the /proverLog command line option".
I use Dafny on Visual Studio, migth I see the VCs from there?

Best,
Paqui
Developer
Oct 31, 2013 at 2:16 PM
Hi Paqui,

you can find out a bit more about the option using Dafny's /help command line option, but usually all you need to do is add /proverLog:log.smt2 to your normal Dafny invocation. The file 'log.smt2' will then contain all the VCs.

Currently, there is no way to produce this log from within Visual Studio.

Best regards,

Valentin
Oct 31, 2013 at 2:42 PM

Thanks again,