A visual inspector for Boogie programs
Márcio Wendel Santana Coêlho, Daniela da Cruz, Pedro Rangel Henriques, Jorge Sousa Pinto · Portuguese National Funding Agency for Science, Research and Technology (RCAAP Project by FCT) · 2011
Design-by-Contract is an approach that allows a program- mer to specify the expected behavior of a component by means of pre- conditions, postconditions and invariants. These annotations (or logical assertions that complement the code) can be seen as a form of enriched software documentation and they can be used to verify that a program is correct with respect to its contracts. Boogie is an intermediate verification language that is being used by more and more software verification tools as a target language. Actually, sev- eral annotation languages are nowadays translated to Boogie language. Despite of its efficiency and popularity, Boogie, that is also a program verifier, does not contain visual information for the user. So, understand- ing how it works is a difficult task. In this paper, we will discuss a visual tool that we developed to help in comprehending Boogie programs.