article

Enabledness and termination in refinement algebra

Authors:

Joakim von WrightAuthors Info & Claims

Science of Computer Programming, Volume 74, Issue 8

Pages 654 - 668

https://doi.org/10.1016/j.scico.2007.11.004

Published: 01 June 2009 Publication History

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.

References

[1]

Aboul-Hosn, K. and Kozen, D.C., KAT-ML: An interactive theorem prover for Kleene algebra with tests. J. Appl. Non-Classical Logics. v16 i1ï¿2. 9-34.

[2]

Back, R.J.R., . In: Mathematical Centre Tracts, vol. 131. Mathematical Centre, Amsterdam.

[3]

Back, R.J.R. and Kurki-Suonio, R., Decentralisation of process nets with centralised control. In: Proc. of 2nd Ann. ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, ACM Press, New York. pp. 131-142.

Digital Library

[4]

Back, R.J.R., A method for refining atomicity in parallel algorithms. In: Odijk, E., Rem, M., Syre, J.-C. (Eds.), Vol. II: Parallel Languages, Lect. Notes in Comput. Sci., vol. 366. Springer, Berlin. pp. 199-216.

Digital Library

[5]

Back, R.~J.~R. and Sere, K., Stepwise refinement of action systems. Struct. Program. v12 i1. 17-30.

[6]

Back, R.J.R. and von Wright, J., Refinement calculus: A systematic introduction. In: Graduate Texts in Computer Science, Springer, New York.

Digital Library

[7]

Back, R.J.R. and von Wright, J., Reasoning algebraically about loops. Acta Inform. v36 i4. 295-334.

[8]

Chen, W. and Udding, J.T., Program inversion: more than fun!. Sci. Comput. Programming. v15 i1. 1-13.

Digital Library

[9]

Cohen, E., Separation and reduction. In: Backhouse, R., Oliveira, J.N. (Eds.), Lect. Notes in Comput. Sci., vol. 1837. Springer, Berlin. pp. 45-59.

Digital Library

[10]

Desharnais, J., Möller, B. and Struth, G., Kleene algebra with domain. ACM Trans. Comput. Logic. v7 i4. 798-833.

Digital Library

[11]

J. Desharnais, B. Möller, G. Struth, Algebraic notions of termination, Technischer Bericht 2006-23, Institut für Informatik, Universität Augsburg, 2006

[12]

Dijkstra, E.W., A Discipline of Programming. 1976. Prentice Hall, Englewood Cliffs.

Digital Library

[13]

Floyd, R.W., Assigning meanings to programs. In: Schwartz, J.T. (Ed.), Proc. of Symp. on Applied Math, vol. 19. Amer. Math. Soc., Providence, RI. pp. 19-32.

[14]

Gries, D., The science of programming. In: Texts and Monographs in Computer Science, Springer, New York.

Digital Library

[15]

Höfner, P. and Struth, G., Automated reasoning in Kleene algebra. In: Pfenning, F. (Ed.), Lect. Notes in Artif. Intell., vol. 4603. Springer, Berlin. pp. 279-294.

Digital Library

[16]

Höfner, P. and Struth, G., Can refinement be automated?. In: Boiten, E.A., Derrick, J., Smith, G. (Eds.), Electron. Notes in Theor. Comput. Sci., vol. 201. pp. 197-222.

Digital Library

[17]

Höfner, P., Möller, B. and Solin, K., Omega algebra, demonic refinement algebra and commands. In: Schmidt, R. (Ed.), Lect. Notes in Comput. Sci., vol. 3125. Springer, Berlin. pp. 222-234.

Digital Library

[18]

Kozen, D., A completeness theorem for Kleene algebras and the algebra of regular events. Inform. and Comput. v110 i2. 366-390.

Digital Library

[19]

Kozen, D., Kleene algebra with tests. ACM Trans. Program. Lang. Syst. v19 i3. 427-443.

Digital Library

[20]

Meinicke, L.A. and Solin, K., Refinement algebra for probabilistic programs. In: Boiten, E.A., Derrick, J., Smith, G. (Eds.), Electron. Notes in Theor. Comput. Sci., vol. 201. pp. 177-195.

Digital Library

[21]

Möller, B., Kleene getting lazy. Sci. Comput. Programming. v65 i2. 195-214.

Digital Library

[22]

Morgan, C.C., . In: Prentice Hall Int. Series in Comput. Sci., Prentice Hall, New York.

[23]

Nelson, G., A generalization of Dijkstraï's calculus. ACM Trans. Program. Lang. Syst. v11 i4. 517-561.

Digital Library

[24]

Solin, K., On two dually nondeterministic refinement algebras. In: Schmidt, R. (Ed.), Lect. Notes in Comput. Sci., vol. 4136. Springer, Berlin. pp. 373-387.

Digital Library

[25]

Solin, K., A sketch of a dynamic epistemic semiring. In: Leivant, D., de Queiroz, R.J.G.B. (Eds.), Lect. Notes in Comput. Sci., vol. 4576. Springer, Berlin. pp. 337-350.

Digital Library

[26]

Solin, K. and von Wright, J., Refinement algebra with operators for enabledness and termination. In: Uustalu, T. (Ed.), Lect. Notes in Comput. Sci., vol. 4014. Springer, Berlin. pp. 397-415.

Digital Library

[27]

von Wright, J., From Kleene algebra to refinement algebra. In: Boiten, E.A., Möller, B. (Eds.), Lect. Notes in Comput. Sci., vol. 2386. Springer, Berlin. pp. 233-262.

Digital Library

[28]

von Wright, J., Towards a refinement algebra. Sci. Comput. Programming. v51 i1ï¿2. 23-45.

Digital Library

Cited By

Solin K(2012)Dual Choice and Iteration in an Abstract Algebra of ActionStudia Logica10.1007/s11225-012-9416-9100:3(607-630)Online publication date: 1-Jun-2012
https://dl.acm.org/doi/10.1007/s11225-012-9416-9
Möller B(2011)Building structured theoriesProceedings of the 12th international conference on Relational and algebraic methods in computer science10.5555/2018285.2018286(1-21)Online publication date: 30-May-2011
https://dl.acm.org/doi/10.5555/2018285.2018286
Preoteasa V(2011)Algebra of monotonic boolean transformersProceedings of the 14th Brazilian conference on Formal Methods: foundations and Applications10.1007/978-3-642-25032-3_10(140-155)Online publication date: 26-Sep-2011
https://dl.acm.org/doi/10.1007/978-3-642-25032-3_10
Show More Cited By

Enabledness and termination in refinement algebra
1. Theory of computation

Recommendations

Refinement Algebra for Probabilistic Programs

We propose an abstract refinement algebra for reasoning about probabilistic programs in a total-correctness setting. The algebra is equipped with operators that determine whether a program is enabled, has certain failure or does not have certain failure,...
Refinement algebra with operators for enabledness and termination
MPC'06: Proceedings of the 8th international conference on Mathematics of Program Construction

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 ...
Refinement algebra for probabilistic programs
Abstract
We identify a refinement algebra for reasoning about probabilistic program transformations in a total-correctness setting. The algebra is equipped with operators that determine whether a program is enabled or terminates respectively. As well as ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Science of Computer Programming

Science of Computer Programming Volume 74, Issue 8

June, 2009

173 pages

ISSN:0167-6423

Issue’s Table of Contents

Copyright © Elsevier B.V. © 2009.

Publisher

Elsevier North-Holland, Inc.

United States

Publication History

Published: 01 June 2009

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Solin K(2012)Dual Choice and Iteration in an Abstract Algebra of ActionStudia Logica10.1007/s11225-012-9416-9100:3(607-630)Online publication date: 1-Jun-2012
https://dl.acm.org/doi/10.1007/s11225-012-9416-9
Möller B(2011)Building structured theoriesProceedings of the 12th international conference on Relational and algebraic methods in computer science10.5555/2018285.2018286(1-21)Online publication date: 30-May-2011
https://dl.acm.org/doi/10.5555/2018285.2018286
Preoteasa V(2011)Algebra of monotonic boolean transformersProceedings of the 14th Brazilian conference on Formal Methods: foundations and Applications10.1007/978-3-642-25032-3_10(140-155)Online publication date: 26-Sep-2011
https://dl.acm.org/doi/10.1007/978-3-642-25032-3_10
Solin K(2010)A sketch of a dynamic epistemic semiringInformation and Computation10.1016/j.ic.2009.03.011208:5(594-604)Online publication date: 1-May-2010
https://dl.acm.org/doi/10.1016/j.ic.2009.03.011

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents