特定の Dafny プログラムが検証するかどうかを問い合わせたいと思います。Dafny は通常、Visual Studio IDE 内でインタラクティブな方法でプログラムを開発するために使用されます。
ただし、非対話的な方法でクエリを実行する必要があります。特に、Python プログラム内から Dafny にクエリを実行する必要があります。これは可能ですか？
1 に答える
1
Python から呼び出しdafny.exeて、検証したい dafny プログラムを含むファイルの名前を引数として渡すことができます。python から外部コマンドを呼び出す方法については、この他の回答を参照してください。
dafny.exeスイッチを指定して実行すると、dafny コマンド ライン引数に関するヘルプが表示されます/?。
検証が成功したかどうかを判断するには、dafny の出力を解析する必要があります。dafny テスト スイートはこのように動作します。
似たようなことをするこのプロジェクトのコードを見てみたいかもしれませんが、Java からのものです。
于 2016-04-06T10:40:28.430 に答える