MURAL - Maynooth University Research Archive Library



    Matching Spec# Specifications


    Li, Peihan (2013) Matching Spec# Specifications. Masters thesis, National University of Ireland Maynooth.

    [img] Download (1MB)


    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...



    Add this article to your Mendeley library


    Abstract

    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.

    Item Type: Thesis (Masters)
    Additional Information: Taught Masters Thesis for the Erasmus Mundus MSc in Dependable Software Systems
    Keywords: Match specifications; Spec# programs; Verification; Design by Contract;
    Academic Unit: Faculty of Science and Engineering > Computer Science
    Item ID: 4553
    Depositing User: IR eTheses
    Date Deposited: 07 Oct 2013 15:57
    URI:
      Use Licence: This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here

      Repository Staff Only(login required)

      View Item Item control page

      Downloads

      Downloads per month over past year

      Origin of downloads