Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/14929
Título: | A visual inspector for Boogie programs |
Autor(es): | Coelho, Márcio Cruz, Daniela da Henriques, Pedro Rangel Pinto, Jorge Sousa |
Palavras-chave: | Program verification Verification condition generators Design-by-contract Boogie Software visualization |
Data: | 2011 |
Resumo(s): | 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. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/14929 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: | DI/CCTC - Artigos (papers) |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
INFORUM-11-b.pdf | Documento principal | 226,64 kB | Adobe PDF | Ver/Abrir |