Homepage>Publikationen>PublikationsDetail

Deriving Partial Correctness Logics From Evolving Algebras

In: B. Pehrson and I. Simoned., IFIP 13th World Computer Congress '94. p. 434--439, Available, August, 1994

Authors

Arnd Poetzsch-Heffter

Abstract

"The paper gives an introduction into the development of partial correctness logics for programming languages specified by evolving algebras. A partial correctness logic is a programming logic that allows to prove program properties of the form: ``whenever program point P is reached during execution, assertion A is true''. We derive a basic axiom (schema) from an evolving algebra and use this axiom to obtain more convenient logics. This work aims to develop the foundations for programming environments that support formal reasoning about programs. One of the major problems with this challenge is the systematic design of programming logics for realistic programming languages. Experiences e.g. with Hoare logic have shown that it can be difficult to design consistent programming logics even for simple languages from scratch. Using evolving algebras as semantical basis has two advantages: They support appropriate specifications of control flow (e.g. for jumps and exceptions). This enables to simplify these aspects in the logic. Proving rules sound w.r.t. a given semantics or systematically deriving rules from semantics specification is simpler than proving the consistency of a logic. Essentially, we relate evolving algebras and temporal logic and apply this combination to develop partial correctness logics. We build on existing approaches to programming logic and on experiences from research on interface specifications for programming languages (e.g. Larch). In this paper, we focus on the dynamic aspects. "

Full Text

PDF: pclea.pdf
PS.GZ: pclea.ps.gz

BibTeX

@InProceedings{Poetzsch-Heffter94deriving, 
   author = {Arnd Poetzsch-Heffter}
   title = {Deriving Partial Correctness Logics From Evolving Algebras},
   booktitle = {IFIP 13th World Computer Congress '94},
   publisher = {Elsevier},
   pages = {434--439},
   note = {Available},
   month = {August},
   year = {1994},
}

Einloggen