Verification, slicing, and visualization of programs with contracts

As a specification carries out relevant information concerning the behaviour of a program, why not explore this fact to slice a program in a semantic sense aiming at optimizing it or easing its verification? It was this idea that Comuzzi, in 1996, introduced with the notion of postcondition-based slicing | slice a program using the information contained in the postcondition (the condition Q that is guaranteed to hold at the exit of a program). After him, several advances were made and different extensions were proposed, bridging the two areas of Program Verification and Program Slicing: specifically precondition-based slicing and specification-based slicing. The work reported in this Ph.D. dissertation explores further relations between these two areas aiming at discovering mutual benefits. A deep study of specification-based slicing has shown that the original algorithm is not efficient and does not produce minimal slices. In this dissertation, traditional specification-based slicing algorithms are revisited and improved (their formalization is proposed under the name of assertion-based slicing), in a new framework that is appropriate for reasoning about imperative programs annotated with contracts and loop invariants. In the same theoretical framework, the semantic slicing algorithms are extended to work at the program level through a new concept called contract based slicing. Contract-based slicing, constituting another contribution of this work, allows for the study of a program at an interprocedural level, enabling optimizations in the context of code reuse. Motivated by the lack of tools to prove that the proposed algorithms work in practice, a tool (GamaSlicer) was also developed. It implements all the existing semantic slicing algorithms, in addition to the ones introduced in this dissertation. This third contribution is based on generic graph visualization and animation algorithms that were adapted to work with verification and slice graphs, two specific cases of labelled control low graphs.

Name thesis:degree_name

Tese de doutoramento em Informática (área de especialização em Ciências da Computação)

Year dc:date.issued

2011

Author dc:creator

• Cruz, Daniela da

Advisors dc:contributor.advisor

• Henriques, Pedro Rangel
• Pinto, Jorge Sousa

Statement dc:rights

• openAccess

Language dc:language.iso

por

Handle dc:identifier.uri

https://hdl.handle.net/1822/19646

OAI record oai:identifier

http://repositorium.sdum.uminho.pt/oai/request?verb=GetRecord&metadataPrefix=dim&identifier=oai%3Arepositorium.uminho.pt%3A1822%2F19646