Kleene algebra with tests
Author:
Open Access
- 1 May 1997
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 19 (3) , 427-443
Abstract
We introduce Kleene algebra with tests, an equational system for manipulating programs. We give a purely equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every while program can be simulated by a while program can be simulated by a while program with at most one while loop. The proof illustrates the use of Kleene algebra with tests and commutativity conditions in program equivalence proofs.Keywords
This publication has 16 references indexed in Scilit:
- A Completeness Theorem for Kleene Algebras and the Algebra of Regular EventsInformation and Computation, 1994
- Equational axioms for regular setsMathematical Structures in Computer Science, 1993
- The Design and Analysis of Algorithms1992
- Complete systems ofB-rational identitiesTheoretical Computer Science, 1991
- A Semiring on Convex Polygons and Zero-Sum Cycle ProblemsSIAM Journal on Computing, 1990
- On the decidability of some problems about rational subsets of free partially commutative monoidsTheoretical Computer Science, 1986
- On folk theoremsCommunications of the ACM, 1980
- Propositional dynamic logic of regular programsJournal of Computer and System Sciences, 1979
- Transductions and Context-Free Languages1979
- Flow diagrams, turing machines and languages with only two formation rulesCommunications of the ACM, 1966