0

I would like to query whether a particular Dafny program verifies. Dafny is typically used to develop programs in an interactive manner inside the visual studio IDE.

However, I need to perform the query in a non-interactive manner. In particular I need to query Dafny from within a python program. Is this possible?

lexicalscope
  • 7,158
  • 6
  • 37
  • 57
Tom
  • 904
  • 1
  • 7
  • 21

1 Answers1

2

You can invoke dafny.exe from python, passing as an argument the name of a file that contains the dafny program that you wish to verify. Please see this other answer on how to call external commands from python.

You can get help on the dafny command line arguments by running dafny.exe with the /? switch.

You will need to parse the output of dafny to determine if the verification was successful. The dafny test suite works in this manner.

You might like to look at the code of this project which does something similar, but from Java.

Community
  • 1
  • 1
lexicalscope
  • 7,158
  • 6
  • 37
  • 57