Matching Spec# Specifications

In this project, we develop a tool which compares two Spec# programs (C# code with specification contracts) for signature matching. The tool automatically identifies whether the two specifications are similar, and gives out a new Spec# program which needs to be verified. There are levels of standards to judge how similar these two Spec# programs’ specification is. This work contributes to the area of code reuse via match specifications: given a specification we aim to mark it to a similar specification and use its implementation to generate the implementation of the original specification. In this work we present the process of match specifications in detail for Spec# programs, we discuss how the method may be applied to other languages and indicate future work in this direction. We match specifications according to the work of Amy Moormann Zaremski and Jeannette M. Wing’s on "Match specifications of Software Components" [1]. This work proposes a lattice of possible technique for match specifications. Examples include Exact Pre/Post Match, Plug-In Match, Plug-In Post Match, Weak Post Match, Exact Predicate Match, Generalized Match and Specialized Match. We apply these definitions to Spec# programs, provide examples of verification matches and illustrate the level of matching that can be achieved automatically within the Spec# tools