MURAL - Maynooth University Research Archive Library



    Matching Spec# Specifications


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

    [thumbnail of Peihan_Li.pdf] PDF
    Peihan_Li.pdf

    Download (1MB)

    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: https://mural.maynoothuniversity.ie/id/eprint/4553
    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)

    Item control page
    Item control page

    Downloads

    Downloads per month over past year

    Origin of downloads