A visual inspector for Boogie programs

• Author(s): Coelho, Márcio ; Cruz, Daniela da ; Henriques, Pedro Rangel ; Pinto, Jorge Sousa
• Date: 2011
• Persistent ID: http://hdl.handle.net/1822/14929
• Origin: RepositóriUM - Universidade do Minho
• Subject(s): Program verification; Verification condition generators; Design-by-contract; Boogie; Software visualization
• Document Type: Article
• Language: English

Description

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.