Abstract
This paper deals with modular verification of component invariants in the B Method. On the one hand, B imposes severe architecture restrictions that ensure soundness of component compositions with a few additional proof obligations. On the other hand, in the context of the verification of object oriented programs, Spec# proposes a more expressive approach, but at the price of more complex specifications, and more numerous proof obligations. In this paper, we investigate an intermediate solution combining the advantages of both approaches.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: The B-Book. Cambridge University Press, Cambridge (1996)
Behm, P., et al.: Météor: A successful application of B in a large project. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369–387. Springer, Heidelberg (1999)
Badeau, F., Amelot, A.: Using B as a High Level Programming Language in an Industrial Project: Roissy VAL. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 334–354. Springer, Heidelberg (2005)
Büchi, M., Back, R.: Compositional Symmetric Sharing in B. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, p. 431. Springer, Heidelberg (1999)
Bert, D., Boulmé, S., Potet, M.-L., Requet, A., Voisin, L.: Adaptable Translator of B Specifications to Embedded C programs. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805. Springer, Heidelberg (2003)
Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6), 27–56 (2004)
Barnett, M., Naumann, D.A.: Friends need a bit more: Maintaining invariants over shared state. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 54–84. Springer, Heidelberg (2004)
Boulmé, S., Potet, M.-L.: Interpreting invariant composition in the B method using the spec# ownership relation: A way to explain and relax B restrictions. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 4–18. Springer, Heidelberg (2006)
ClearSy. Le Langage B. Manuel de reference, version 1.8.5. ClearSy (2002)
Dijkstra, E.W.: A discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Gries, D., Prins, J.: A New Notion of Encapsulation. In: Proc. of Symposium on Languages Issues in Programming Environments, SIGLPAN (1985)
Habrias, H.: Spécification formelle avec B. Hermès Science Publications (2001)
Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1, 271–281 (1972)
Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–516. Springer, Heidelberg (2004)
Leino, K.R.M., Müller, P.: A verification methodology for model fields. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 115–130. Springer, Heidelberg (2006)
Lanet, J.-L., Requet, A.: Formal Proof of Smart Card Applets Correctness. In: Schneier, B., Quisquater, J.-J. (eds.) CARDIS 1998. LNCS, vol. 1820. Springer, Heidelberg (2000)
Morgan, C., Gardiner, P.H.B.: Data Refinement by Calculation. Acta Informatica 27(6), 481–503 (1990)
Müller, P., Poetzsch-Heffer, A., Leavens, G.T.: Modular Invariants for Layered Object Structures. Science of Computer Programming (2006)
Naumann, D.A., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state. In: LICS 2004, pp. 313–323. IEEE Computer Society Press, Los Alamitos (2004)
Potet, M.-L.: Spécifications et développements formels: Etude des aspects compositionnels dans la méthode B. Habilitation à diriger des recherches, Institut National Polytechnique de Grenoble, décembre 5 (2002)
Sabatier, D., Lartigue, P.: The Use of the B method for the Design and the Validation of the Transaction Mechanism for smart Card Applications. Formal Methods in System Design 17(3), 245–272 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Boulmé, S., Potet, ML. (2009). Relaxing Restrictions on Invariant Composition in the B Method by Ownership Control a la Spec# . In: Abrial, JR., Glässer, U. (eds) Rigorous Methods for Software Construction and Analysis. Lecture Notes in Computer Science, vol 5115. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11447-2_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-11447-2_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11446-5
Online ISBN: 978-3-642-11447-2
eBook Packages: Computer ScienceComputer Science (R0)