Abstract
The B concept of generalised substitutions is applied to expressions as well as predicates to obtain “expression transformers”, which formalise the idea of speculative computation and form part of the executable subset of our language. We define expression transformers over the syntactic constructs of B-GSL, and show this definition is equivalent to an alternative based on before-after predicates. The use of expression transformers is illustrated by example programs which combine functional and imperative programming styles and exploit backtracking.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Jean-Raymond Abrial. The B Book. Cambridge University Press, 1996.
E C R Hehner. Bunch theory: A simple set theory for computer science. Information Processing Letters, 12.1 pp26–31, 1981.
E C R Hehner. A Practical Theory of Programming. Springer Verlag, 1993.
http://www.haskell.org. Haskell98, a non-strict purely functional language. Technical report, 1998.
J M Lucassen. Types and Effects, towards the integration of functional and imperitive programming. PhD thesis, MIT laboratory for computer science, 1987.
E Moggi. Notions of Computation and Monads. Information and Computation 93(1), 1991.
J Morris and A Bunkenburg. A theory of bunches. Acta Informatica, 37(8).
J M Morris. An easy route from functional to imperative programming. Presented at the 5th Irish Formal Methods Workshop, Trinity College, Dublin, July 2001.
J M Morris and A Bunkenburg. Term transformer semantics. Submitted to ACM Transactions on Programming Languages and Systems, 1999.
Greg Nelson. A Generalization of Dijkstra’s Calculus. ACM Transactions on Programming Languages and Systems, Vol 11, No. 4, 1989.
W J Stoddart. An Execution Architecture for B-GSL. In Bowen J and Dunne S E, editors, ZB2000, Lecture Notes in Computer Science, no 1878, 2000.
W J Stoddart. Efficient reversibility with guards and choice. In M A Ertl, editor, 18th EuroForth, 2002. Available from: http://www.complang.tuwien.ac.at/anton/euroforth2002/papers/bill.rev.ps.gz.
W J Stoddart and F Zeyda. Implementing sets for reversible computation. In M A Ertl, editor, 18th EuroForth, 2002. Available from: http://www.complang.tuwien.ac.at/anton/euroforth2002/papers/bill.sets.ps.gz.
P Wadler. Monads for functional programming. In J Jeuring and E Meijer, editors, Advanced Functional Programming, Lecture notes in Computer Science, no 925, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stoddart, B., Zeyda, F. (2003). Expression Transformers in B-GSL. In: Bert, D., Bowen, J.P., King, S., Waldén, M. (eds) ZB 2003: Formal Specification and Development in Z and B. ZB 2003. Lecture Notes in Computer Science, vol 2651. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44880-2_14
Download citation
DOI: https://doi.org/10.1007/3-540-44880-2_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40253-4
Online ISBN: 978-3-540-44880-8
eBook Packages: Springer Book Archive