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. © 2009 Springer-Verlag.
CITATION STYLE
Boulmé, S., & Potet, M. L. (2009). Relaxing restrictions on invariant composition in the B method by ownership control a la Spec#. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5115 LNCS, pp. 1–16). https://doi.org/10.1007/978-3-642-11447-2_1
Mendeley helps you to discover research relevant for your work.