Type Synthesis in B and the Translation of B to PVS
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.
KeywordsB semantics logical frameworks type theory PVS
Unable to display preview. Download preview PDF.
- [Abr96]J.R. Abrial. The B-Book Assigning programs to meanings. Cambridge University Press, 1996.Google Scholar
- [Age96]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.Google Scholar
- [BBC+97]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.
- [BFM99]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.Google Scholar
- [BG94]J. Bowen and M. Gordon. Z and HOL. In 8th Z User Meeting (ZUM’94). BCS FACS, June 1994.Google Scholar
- [CC77]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.Google Scholar
- [Cha98]P. Chartier. Formalisation of B in Isabelle/HOL. In Proc. Second B International Conference, Montpellier, France, 1998.Google Scholar
- [COR+95]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.
- [Cou00]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.
- [DBMM00]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.CrossRefGoogle Scholar
- [DDG98]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.Google Scholar
- [DT00a]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.Google Scholar
- [DT00b]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.Google Scholar
- [GM94]M.J.C. Gordon and T.F. Melham. Introduction to HOL. http://www.cl.cam.ac.uk/Research/HVG/HOL. Cambridge University Press, 1994.
- [Gor94]M.J.C. Gordon. Merging hol with set theory: preliminary experiments. Technical Report 353, University of Cambridge Computer Laboratory, 1994.Google Scholar
- [KB95]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.Google Scholar
- [KSW96]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.Google Scholar
- [Mar01]G Mariano. The Bcaml project. Technical report, INRETS, http://www3.inrets.fr/Public/ESTAS/Mariano.Georges, 2001.
- [MB97]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.Google Scholar
- [Pau92]L.C. Paulson. Introduction to Isabelle. Technical report, Computer laboratory, university of Cambrige, 1992.Google Scholar
- [PR98]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.Google Scholar
- [Reg95]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.Google Scholar
- [Rou99]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.Google Scholar