671
views
0
recommends
+1 Recommend
1 collections
    4
    shares
       
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      A Tool for Logic Program Refinement

      proceedings-article
      , , ,
      Proceedings of the 2nd BCS-FACS Northern Formal Methods (FM)
      Northern Formal Methods
      14-15 July 1997
      Bookmark

            Abstract

            The refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In the original refinement calculus, the target language is an imperative programming language, but more recently a refinement calculus for deriving logic programs has been proposed. Due to the amount of detail involved, the manual refinement of programs is a tedious and time- consuming task, and is therefore an obvious candidate for tool support. Several tools exist for the imperative refinement calculus, and in this paper we describe a prototype tool to support the recently developed refinement calculus for logic programs. The tool was developed using Ergo, an interactive theorem prover. To provide tool support for the calculus, its underlying semantic model was defined within Ergo, and the laws of the calculus were proven in that framework. We illustrate the tool using a simple example refinement.

            Content

            Author and article information

            Conference
            July 1997
            July 1997
            : 1-18
            Affiliations
            [0001]Software Verification Research Centre

            School of Information Technology

            University of Queensland, Brisbane, 4072, Australia
            Article
            10.14236/ewic/FA1997.3
            8148b2d7-923a-4c68-9bcb-f034614e63e9
            © Robert Colvin et al. Published by BCS Learning and Development Ltd. Proceedings of the 2nd BCS-FACS Northern Formal Methods Workshop, Ilkley

            This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

            Proceedings of the 2nd BCS-FACS Northern Formal Methods
            FM
            2
            Ilkley
            14-15 July 1997
            Electronic Workshops in Computing (eWiC)
            Northern Formal Methods
            Product
            Product Information: 1477-9358BCS Learning & Development
            Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/FA1997.3
            Self URI (journal page): https://ewic.bcs.org/
            Categories
            Electronic Workshops in Computing

            Applied computer science,Computer science,Security & Cryptology,Graphics & Multimedia design,General computer science,Human-computer-interaction

            Comments

            Comment on this article