Article ID Journal Published Year Pages File Type
434514 Science of Computer Programming 2009 15 Pages PDF
Abstract

Refinement algebras are abstract algebras for reasoning about programs in a total correctness framework. We extend a reduct of von Wright’s demonic refinement algebra with two operators for modelling enabledness and termination of programs. We show how the operators can be used for expressing relations between programs and apply the algebra to reasoning about action systems.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics