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

      A Simple Algorithm Specification Language and its Application

      Proceedings of the 1st Irish Workshop on Formal Methods (FM)

      Irish Workshop on Formal Methods

      3-4 July 1997

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          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.

          Related collections

          Most cited references 5

          • Record: found
          • Abstract: not found
          • Article: not found

          An axiomatic basis for computer programming

           C. Hoare (1969)
            Bookmark
            • Record: found
            • Abstract: not found
            • Book Chapter: not found

            Automating Recursive Type Definitions in Higher Order Logic

              Bookmark
              • Record: found
              • Abstract: not found
              • Book Chapter: not found

              Mechanizing Programming Logics in Higher Order Logic

                Bookmark

                Author and article information

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

                Cambridge, England
                Article
                10.14236/ewic/FM1997.4
                © 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
                Product
                Product Information: 1477-9358BCS Learning & Development
                Self URI (journal page): https://ewic.bcs.org/
                Categories
                Electronic Workshops in Computing

                Comments

                Comment on this article