Dafnyは非対話的に、例えばPythonプログラムから使用できますか？

Question

特定のDafnyプログラムが確認するかどうかを問い合わせたいと思います。 Dafnyは、通常、ビジュアルスタジオIDE内でインタラクティブにプログラムを開発するために使用されます。

しかし、非対話的な方法でクエリを実行する必要があります。特に私はPythonプログラムの中からDafnyに問い合わせる必要があります。これは可能ですか？

Answer 1

dafny.exeは、検証するdafnyプログラムを含むファイルの名前を引数として渡して、pythonから呼び出すことができます。このother answer on how to call external commands from pythonをご覧ください。

スイッチでdafny.exeを実行すると、dafnyコマンドライン引数に関するヘルプが表示されます。

あなたはの出力を解析し、検証が成功したかどうかを確認する必要があります。 dafny test suiteはこのように動作します。

何か似ていますが、Javaからはcode of this projectを見てください。