• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Reasoning Algebraically about Loops

Ralph-Johan Back, Joakim von Wright, Reasoning Algebraically about Loops. Acta Informatica 36, 295–334, 1999.

Abstract:

We show how to formalise different kinds of loop constructs
within
the refinement calculus, and how to use this formalisation to derive
general transformation rules for loop constructs. The emphasis is
on using algebraic methods for reasoning about equivalence and refinement
of loop constructs, rather than operational ways of reasoning about
loops in terms of their execution sequences. We apply the algebraic
reasoning techniques to derive a collection of transformation rules
for action systems and for guarded loops. These include transformation
rules that have been found important in practical program derivations:
data refinement and atomicity refinement of action systems; and merging,
reordering, and data refinement of loops with stuttering transitions.

Files:

Full publication in PDF-format

BibTeX entry:

@ARTICLE{jBaWr99a,
  title = {Reasoning Algebraically about Loops},
  author = {Back, Ralph-Johan and Wright, Joakim von},
  journal = {Acta Informatica},
  volume = {36},
  pages = {295–334},
  year = {1999},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Publication Forum rating of this publication: level 2

Edit publication