Abstract
In this paper, we study the design of a typed functional semantics for B. Our aim is to reuse the well known logical frameworks based on higher order logic, e.g., Isabelle, Coq and PVS as proving environments for B. We consider type synthesis for B and study a semantics and some of its composition mechanisms by translation to PVS.
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
J.R. Abrial. The B-Book Assigning programs to meanings. Cambridge University Press, 1996.
Agerholm, S. Translating specifications in VDM-SL to PVS. In J. Grundy J. VonWright and J. Harisson, editors, Proceeding of the 9th International Conference On Theorem Proving in Higher Order Logics, volume 1125 of Lecture Notes in Computer Science, pages 1–16, Turku, Finland, 1996. Springer-Verlag.
B. Barras, S. Boutin, C. Cornes, J. Courant, J.C. Filliatre, E. Giménez, H. Herbelin, G. Huet, C. Muńoz, C. Murthy, C. Parent, C. Paulin, A. Saïbi, and B. Werner. The Coq Proof Assistant Reference Manual — Version V6.1. Technical Report 0203, INRIA, August 1997. http://coq.inria.fr.
J.-P. Bodeveix, M. Filali, and C. Munoz. A formalization of the B method in Coq and PVS. In FM’99-B Users Group Meeting — Applying B in an industrial context: Tools, Lessons and Techniques, pages 32–48, 1999.
J. Bowen and M. Gordon. Z and HOL. In 8th Z User Meeting (ZUM’94). BCS FACS, June 1994.
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pages 238–252, Los Angeles, California, 1977. ACM Press, New York, NY.
P. Chartier. Formalisation of B in Isabelle/HOL. In Proc. Second B International Conference, Montpellier, France, 1998.
S. Crow, S. Owre, J. Rushby, N. Shankar, and S. Mandayam. A Tutorial Introduction to PVS. In Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, http://www.csl.sri.com/pvs, April 1995.
P. Cousot. Abstract interpretation: Achievements and perspectives. In Proceedings of the SSGRR 2000 Computer & eBusiness International Conference, Compact disk paper 224 and electronic proceedings http://www.ssgrr.it/en/ssgrr2000/proceedings.htm, L’’Aquila, Italy, July 31-August 6 2000. Scuola Superiore G. Reiss Romoli.
T. Dimitrakos, J. Bicarregui, B. Matthews, and Maibaum. Compositional structuring in the B-method: A logical viewpoint of the static context. In J.-P. Bowen, S. Dunne, A. Galloway, and S. King, editors, ZB’2000: Formal Specification and Development in Z and B, volume 1878 of Lecture Notes in Computer Science. Springer-Verlag, September 2000.
C. Dubois and V. Donzeau-Gouge. A step towards the mechanization of partial functions: domains as inductive predicates. In In Workshop on mechanization of partial functions, CADE 15, July 1998.
D. Duffy and I. Toyn. Reasoning inductively about Z specifications via unification. In Proceedings International Conference of Z and B Users, ZB2000, volume 1878 of Lecture Notes in Computer Science. Springer-Verlag, May 2000.
D. Duffy and I. Toyn. Typechecking Z. In Proceedings International Conference of Z and B Users, ZB2000, volume 1878 of Lecture Notes in Computer Science. Springer-Verlag, May 2000.
M.J.C. Gordon and T.F. Melham. Introduction to HOL. http://www.cl.cam.ac.uk/Research/HVG/HOL. Cambridge University Press, 1994.
M.J.C. Gordon. Merging hol with set theory: preliminary experiments. Technical Report 353, University of Cambridge Computer Laboratory, 1994.
I. Kraan and P. Baumann. Implementing Z in Isabelle. In Bowen and Hinchey, editors, ZUM’95: The Z formal specification notation, number 967 in Lecture Notes in Computer Science, pages 355–373. Springer-Verlag, 1995.
Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle/HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics — 9th International Conference, volume 1125of Lecture Notes in Computer Science, pages 283–298. Springer Verlag, 1996.
G Mariano. The Bcaml project. Technical report, INRETS, http://www3.inrets.fr/Public/ESTAS/Mariano.Georges, 2001.
S. Maharaj and J. Bicarregui. On verification of VDM specification and refinement with PVS. In proceedings of the 12th IEEE International Conference in Automated Software Engineering, pages 280–289, 1997.
O. Müller and K. Slind. Treating partiality in a logic of total functions. The Computer Journal, 40(10):1–12, 1997.
L.C. Paulson. Introduction to Isabelle. Technical report, Computer laboratory, university of Cambrige, 1992.
Lawrence C. Paulson. Set theory for verification: I. From foundations to functions. Journal of Automated Reasoning, 11(3):353–389, 1993.
M.-L. Potet and Y. Rouzaud. Composition and refinement in the Bmethod. volume 1393 of Lecture Notes in Computer Science, pages 46–65. Springer-Verlag, 1998.
F. Regensburger. HOLCF: Higher Order Logic of Computable Functions. In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors, Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, number 971 in Lecture Notes in Computer Science, Aspen Grove, Utah, 1995. Springer-Verlag.
Y. Rouzaud. Interpreting the B-method in the refinement calculus. In J. Wing, J. Woodcock, and J. Davies, editors, FM’99, volume 1708 of Lecture Notes in Computer Science, pages 411–430. Springer-Verlag, Sep 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bodeveix, JP., Filali, M. (2002). Type Synthesis in B and the Translation of B to PVS. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds) ZB 2002:Formal Specification and Development in Z and B. ZB 2002. Lecture Notes in Computer Science, vol 2272. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45648-1_18
Download citation
DOI: https://doi.org/10.1007/3-540-45648-1_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43166-4
Online ISBN: 978-3-540-45648-3
eBook Packages: Springer Book Archive