GamaBoogie : a contract-based slicer for Boogie programs
Márcio Wendel Santana Coêlho · Portuguese National Funding Agency for Science, Research and Technology (RCAAP Project by FCT) · 2011
In the context of the Informatics Engineering MSc. degree (MEI), second year, this document describes and discusses a master thesis project in the area of source code analysis using slicing and program verification techniques. Design-by-Contract is an approach that allows a programmer to specify the expected behaviour of a component by the means of preconditions, postconditions and invariants. These annotations (or contracts) can be seen as a form of enriched software documentation and they are used to verify that the program is correct with respect to these contracts. On one hand, slicing the program to extract the code that is relevant for the contracts reduce the size of the program and improves its verification. On the other hand, using the contract to slice a program in a finer, more sensible semantic way, enables to optimise the code reducing it to the minimum necessary to keep the postcondition true. Following the last research direction, Daniela da Cruz introduced in her Ph.D. thesis the concepts of Assertion-based Slicing and Contract-based Slicing to explore (at an intra-procedural or interprocedural level) the optimisation of code according to the semantics expressed by contracts. Her approach is based on the source code analyses and her slicing uses annotations present in the procedures. This thesis focuses on the study of BoogiePL language and its use as an intermediate representation for annotated programs in order to build slices of Boogie programs (instead of slicing the source code). Boogie compiler is used to generate the verification conditions in SMT just for the computed slice; these conditions can be then passed to the Z3 Prover to ensure that all contracts are preserved when invoking annotated procedures. The final objective is to make possible the comparison between the SMT code produced by this approach and the code currently generated by GamaSlicer, expecting to obtain a more efficient solution. To implement that idea, a tool called GamaBoogie was developed. That tool, at the end, offers more than its main functionality in slicing and verifying. Actually it allows to inspect and visualise boogie programs; this functionality seems to be very useful for Boogie program comprehension.