제 질문은 Boogie에 관한 것이지만, Boogie 태그를 사용할 수 없기 때문에 Boogie와 밀접한 관련이있는 것으로 dafny 태그를 사용했습니다.
설명서의 지침에 따라 Visual Studio에서 Boogie를 빌드했습니다. Boogie 코드를 작성하려면 다음에 무엇을해야하나요? 아니면 Test 폴더에서 .bpl 파일을 어떻게 실행할 수 있나요? 내가 이해 한 바에 따르면 Boogie는 중간 검증 언어도 독립적으로 사용할 수 있습니다.
감사합니다.
Boogie에는 대화 형 VS 모드가 없습니다. Boogie 코드를 작성하고 편집기에서 디자인 타임 피드백을 받으려면 사용 가능한 최상의 모드는 emacs 입니다. https://github.com/boogie-org/boogie-friends를 참조 하십시오 . 그래도이 emacs 모드는 오류 추적이나 검증 디버거 정보를 제공하지 않습니다.
이 기사는 인터넷에서 수집됩니다. 재 인쇄 할 때 출처를 알려주십시오.
침해가 발생한 경우 연락 주시기 바랍니다[email protected] 삭제
몇 마디 만하겠습니다