Буги-вуги в Visual Studio

Мой вопрос о буги-вуги, но поскольку тега буги не было, я использовал тег dafny как тесно связанный с буги-вуги.

Я построил Boogie в Visual Studio, следуя инструкциям в документации. Что мне делать дальше, чтобы написать код Boogie или, что то же самое, как я могу запустить файлы .bpl в тестовой папке? Из того, что я понял, так это то, что Boogie, хотя и промежуточный язык проверки, также может использоваться независимо.

Спасибо.


z3 dafny
person notArefill    schedule 18.03.2017    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Для Boogie нет интерактивного режима VS. Если вы хотите писать код Boogie и получать обратную связь во время разработки в редакторе, лучший доступный режим — это emacs, см. https://github.com/boogie-org/boogie-friends. Тем не менее, этот режим emacs не дает вам трассировки ошибок или информации отладчика проверки.

person Rustan Leino    schedule 20.03.2017
comment
Спасибо, на emacs уже настраивал буги-френдс, и искал что-то подобное на VS. Правильно ли я предполагаю, что функция на emacs, где вы можете увидеть переведенный код dafny, недоступна в VS? - person notArefill; 21.03.2017

arrow_upward
0
arrow_downward

Boogie зависит от Z3, поэтому убедитесь, что он доступен.

Затем из командной строки:

  • boogie.exe /help
  • boogie.exe file_to_verify.bpl
person Malte Schwerhoff    schedule 20.03.2017
comment
Спасибо, я запускаю его из командной строки, как мне это сделать из Visual Studio? Как я могу увидеть эти следы проверки от VS? Подсветка синтаксиса и прочее. - person notArefill; 20.03.2017
comment
Без понятия, извини. - person Malte Schwerhoff; 20.03.2017