Enabledness and termination in refinement algebra |
| |
Authors: | Kim Solin Joakim von Wright |
| |
Affiliation: | Dept. of IT, Åbo Akademi, Joukahainengatan 3-5, FIN-20520 Åbo, Finland |
| |
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. |
| |
Keywords: | Refinement algebra Enabledness Termination Action systems |
本文献已被 ScienceDirect 等数据库收录! |