View in EDS

Building program construction and verification tools from algebraic principles.

Saved in:
Bibliographic Details
Title: Building program construction and verification tools from algebraic principles.
Authors: Armstrong, Alasdair1, Gomes, Victor1, Struth, Georg1 g.struth@sheffield.ac.uk
Source: Formal Aspects of Computing. Apr2016, Vol. 28 Issue 2, p265-293. 29p.
Subjects: Imperative programming, Kleene algebra, Data flow computing, Semantic computing, Recursive functions
Abstract: We present a principled modular approach to the development of construction and verification tools for imperative programs, in which the control flow and the data flow are cleanly separated. Our simplest verification tool uses Kleene algebra with tests for the control flow of while-programs and their standard relational semantics for the data flow. It is expanded to a basic program construction tool by adding an operation for the specification statement and one single axiom. To include recursive procedures, Kleene algebras with tests are expanded further to quantales with tests. In this more expressive setting, iteration and the specification statement can be defined explicitly and stronger program transformation rules can be derived. Programming our approach in the Isabelle/HOL interactive theorem prover yields simple lightweight mathematical components as well as program construction and verification tools that are correct by construction themselves. Verification condition generation and program construction rules are based on equational reasoning and supported by powerful Isabelle tactics and automated theorem proving. A number of examples shows our tools at work. [ABSTRACT FROM AUTHOR]
Copyright of Formal Aspects of Computing is the property of Association for Computing Machinery and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 114327189
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Building program construction and verification tools from algebraic principles.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Armstrong%2C+Alasdair%22">Armstrong, Alasdair</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22Gomes%2C+Victor%22">Gomes, Victor</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22Struth%2C+Georg%22">Struth, Georg</searchLink><relatesTo>1</relatesTo><i> g.struth@sheffield.ac.uk</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Formal+Aspects+of+Computing%22">Formal Aspects of Computing</searchLink>. Apr2016, Vol. 28 Issue 2, p265-293. 29p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Imperative+programming%22">Imperative programming</searchLink><br /><searchLink fieldCode="DE" term="%22Kleene+algebra%22">Kleene algebra</searchLink><br /><searchLink fieldCode="DE" term="%22Data+flow+computing%22">Data flow computing</searchLink><br /><searchLink fieldCode="DE" term="%22Semantic+computing%22">Semantic computing</searchLink><br /><searchLink fieldCode="DE" term="%22Recursive+functions%22">Recursive functions</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: We present a principled modular approach to the development of construction and verification tools for imperative programs, in which the control flow and the data flow are cleanly separated. Our simplest verification tool uses Kleene algebra with tests for the control flow of while-programs and their standard relational semantics for the data flow. It is expanded to a basic program construction tool by adding an operation for the specification statement and one single axiom. To include recursive procedures, Kleene algebras with tests are expanded further to quantales with tests. In this more expressive setting, iteration and the specification statement can be defined explicitly and stronger program transformation rules can be derived. Programming our approach in the Isabelle/HOL interactive theorem prover yields simple lightweight mathematical components as well as program construction and verification tools that are correct by construction themselves. Verification condition generation and program construction rules are based on equational reasoning and supported by powerful Isabelle tactics and automated theorem proving. A number of examples shows our tools at work. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Formal Aspects of Computing is the property of Association for Computing Machinery and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=114327189
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1007/s00165-015-0343-1
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 29
        StartPage: 265
    Subjects:
      – SubjectFull: Imperative programming
        Type: general
      – SubjectFull: Kleene algebra
        Type: general
      – SubjectFull: Data flow computing
        Type: general
      – SubjectFull: Semantic computing
        Type: general
      – SubjectFull: Recursive functions
        Type: general
    Titles:
      – TitleFull: Building program construction and verification tools from algebraic principles.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Armstrong, Alasdair
      – PersonEntity:
          Name:
            NameFull: Gomes, Victor
      – PersonEntity:
          Name:
            NameFull: Struth, Georg
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 04
              Text: Apr2016
              Type: published
              Y: 2016
          Identifiers:
            – Type: issn-print
              Value: 09345043
          Numbering:
            – Type: volume
              Value: 28
            – Type: issue
              Value: 2
          Titles:
            – TitleFull: Formal Aspects of Computing
              Type: main
ResultId 1