在Visual Studio上的布吉

2017-03-18 59 views 0 likes

我的問題是關於布吉，但由於沒有布吉標籤可用，我使用了與布吉密切相關的dafny標籤。在Visual Studio上的布吉

我按照文檔中的說明在Visual Studio上構建了Boogie。我應該在下一步做什麼來編寫Boogie代碼，或者等價地如何在Test文件夾中運行.bpl文件？從我的理解是，布吉雖然也可以獨立使用中間驗證語言。

謝謝。

2017-03-18 notArefill

回答

沒有互動VS模式布吉。如果您想編寫Boogie代碼並在編輯器中獲得設計時反饋，那麼可用的最佳模式是在emacs中，請參閱https://github.com/boogie-org/boogie-friends。不過，這個emacs模式不會給你錯誤跟蹤或驗證調試信息。

2017-03-20 22:43:16

謝謝，我已經在emacs上設置了boogie-friends，並在VS上尋找類似的東西。我是否正確地認爲在emacs上可以看到已翻譯的dafny代碼的功能在VS上不可用？ – notArefill

布吉取決於Z3，所以請確保它可用。

然後，從命令行：

2017-03-20 08:19:16

謝謝，我從命令行運行它，我怎麼能從Visual Studio中做到這一點？我怎樣才能看到來自VS的驗證痕跡？語法突出顯示和其餘部分。 – notArefill

不知道，對不起。 –

相關問題