1,234
views
0
recommends
+1 Recommend
1 collections
    0
    shares

      Celebrating 65 years of The Computer Journal - free-to-read perspectives - bcs.org/tcj65

      scite_
       
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      A Simple Algorithm Specification Language and its Application

      proceedings-article
      Proceedings of the 1st Irish Workshop on Formal Methods (FM)
      Irish Workshop on Formal Methods
      3-4 July 1997
      Bookmark

            Abstract

            A pragmatic approach to algorithm specification and verification is presented. The language AL provides a level of abstraction between a mathematical specification notation and a programming language, supporting compact but expressive algorithm description. Proofs of correctness about algorithms written in AL can be done via an embedding of the semantics of the language in a proof system; implementations of algorithms can be done through translation to standard programming languages. The proofs of correctness are more tractable than direct verification of programming language code; descriptions in AL are more easily related to executable programs than standard mathematical specifications. AL provides an independent, portable description which can be related to different proof systems and different programming languages. Several interfaces have been explored and tools for fully automatic translation of AL specifications into the HOL logic and Standard ML executable code have been implemented. A substantial case study uses AL as the common specification language from which both the formal proofs of correctness and executable code have been produced.

            Content

            Author and article information

            Conference
            September 1997
            September 1997
            : 1-19
            Affiliations
            [0001]Cambridge Computer Science Research Centre, SRI International

            Cambridge, England
            Article
            10.14236/ewic/FM1997.4
            a7ec7313-9cd0-4cec-8ca5-d24cf51a3496
            © John Herbert. Published by BCS Learning and Development Ltd. Proceedings of the 1st Irish Workshop on Formal Methods, Dublin

            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 1st Irish Workshop on Formal Methods
            FM
            1
            Dublin
            3-4 July 1997
            Electronic Workshops in Computing (eWiC)
            Irish Workshop on Formal Methods
            History
            Product

            1477-9358 BCS Learning & Development

            Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/FM1997.4
            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