Program slicing is a decomposition technique that extracts from a program the statements relevant to a particular computation.
A program slice consists of the parts of a program that potentially affect the values computed at some point of interest referred to as a slicing criterion.

In Weiser\'s approach, slices are built by computing consecutive sets of transitively relevant statements, according to data flow and control flow dependencies. Only statically available information is used for computing slices. In case of dynamic slicing, it considers a specific input for the variables under consideration (it gives context, not semantic).
Semantic slicing is more powerful and flexible than syntactic slicing, since the criteria can be as expressive as any set of first-order formulas on the initial and final states of the program.

GamaSlicer is a framework designed by Daniela da Cruz, that includes a Verification Condition Generator (VCGen), a parameterizable slicer with a choice of algorithms, and a visualisation functionality. It works on Java programs with JML annotations (the standard specification language for Java ).
Instead of programs consisting of sets of procedures, one has classes with their methods, sharing a set of class/instance variables instead of global variables.

GamaBoogie is a framework to slice the intermediate Boogie program. This tool generates 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. Moreover, GamaBoogie 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.

The current version of GamaBoogie is available as a desktop version. You can download it here.

Check out some screenshots of GamaSlicer in this Gallery.

Slicing Algorithm in GamaBoogie

  • Specification-based slicing (introduced by Chung et al in Program slicing based on specification) --- A program S1 is a specification based slice of S2 with respect to the given pre-postcondition pair (P;Q) if S1 preserves the correctness of S2 for (P;Q) and S1 can be obtained from S2.

GamaBoogie GUI

  • Tab 1 contains the Spec# source program to be analyzed.
  • Tab 2 contains the Boogie source program to be analyzed.
  • Tab 3 contains the Identifier Table built during the analysis phase.
  • Tab 4 displays the control flow graph (CFG) as the visual representation of the program, giving an immediate and clear perception of the program complexity, with its procedures and the relationships among them.
  • Tab 5 display the Weakest PreCondictions (WP)
  • Tab 6 display the passify commands
  • Tab 7 display the relation between the WP and passify commands