{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:47:48Z","timestamp":1725475668882},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540687603"},{"type":"electronic","value":"9783540687610"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11955757_4","type":"book-chapter","created":{"date-parts":[[2006,12,11]],"date-time":"2006-12-11T09:34:20Z","timestamp":1165829660000},"page":"4-18","source":"Crossref","is-referenced-by-count":4,"title":["Interpreting Invariant Composition in the B Method Using the Spec# Ownership Relation: A Way to Explain and Relax B Restrictions"],"prefix":"10.1007","author":[{"given":"Sylvain","family":"Boulm\u00e9","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marie-Laure","family":"Potet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book. Cambridge University Press, Cambridge (1996)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-48119-2_22","volume-title":"FM\u201999 - Formal Methods","author":"P. Behm","year":"1999","unstructured":"Behm, P., et al.: M\u00e9t\u00e9or: A Successful Application of B in a Large Project. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 348\u2013387. Springer, Heidelberg (1999)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"F. Badeau","year":"2005","unstructured":"Badeau, F., Amelot, A.: Using B in a High Level Programming Language in an Industrial Project: Roissy VAL. In: Treharne, H., King, S., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol.\u00a03455, Springer, Heidelberg (2005)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48119-2_25","volume-title":"FM\u201999 - Formal Methods","author":"M. B\u00fcchi","year":"1999","unstructured":"B\u00fcchi, M., Back, R.: Compositional Symmetric Sharing in B. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, Springer, Heidelberg (1999)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-44880-2","volume-title":"FME 2003: Formal Methods","author":"D. Bert","year":"2003","unstructured":"Bert, D., Boulm\u00e9, 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.\u00a02805, Springer, Heidelberg (2003)"},{"issue":"6","key":"4_CR6","doi-asserted-by":"publisher","first-page":"27","DOI":"10.5381\/jot.2004.3.6.a2","volume":"3","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology\u00a03(6), 27\u201356 (2004)","journal-title":"Journal of Object Technology"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27764-4_5","volume-title":"Mathematics of Program Construction","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., Naumann, D.A.: Friends need a bit more: Maintaining invariants over shared state. In: Kozen, D. (ed.) MPC 2004. LNCS, vol.\u00a03125, Springer, Heidelberg (2004)"},{"key":"4_CR8","unstructured":"ClearSy. Le Langage B. Manuel de reference, version 1.8.5. ClearSy (2002)"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Doll\u00e9, D., Essam\u00e9, D., Falampin, J.: B \u00e0 Siemens Transportation Systems- Une exp\u00e9rience industrielle. In: D\u00e9veloppement rigoureux de logiciel avec la m\u00e9thode B, vol.\u00a022, Technique et Science Informatiques (2003)","DOI":"10.3166\/tsi.22.11-32"},{"key":"4_CR10","volume-title":"A discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Gries, D., Prins, J.: A New Notion of Encapsulation. In: Proc. of Symp. on Languages Issues in Programming Environments, SIGLPAN (1985)","DOI":"10.1145\/800225.806834"},{"key":"4_CR12","unstructured":"Habrias, H.: Sp\u00e9cification formelle avec B. Herm\u00e8s Science (2001)"},{"key":"4_CR13","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica\u00a01, 271\u2013281 (1972)","journal-title":"Acta Informatica"},{"key":"4_CR14","volume-title":"Behavioral Specifications of Businesses and Systems","author":"G. Leavens","year":"1999","unstructured":"Leavens, G., Baker, A., Ruby, C.: JML: A notation for detailed design. In: Behavioral Specifications of Businesses and Systems, Kluwer Academic Publishers, Dordrecht (1999)"},{"key":"4_CR15","unstructured":"Leavens, G., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical report, TR 98-06i, Iowa State University (2000)"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-24851-4_22","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"K.R.M. Leino","year":"2004","unstructured":"Leino, K.R.M., M\u00fcller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 491\u2013516. Springer, Heidelberg (2004)"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10721064_7","volume-title":"Smart Card. Research and Applications","author":"J.-L. Lanet","year":"2000","unstructured":"Lanet, J.-L., Requet, A.: Formal Proof of Smart Card Applets Correctness. In: Schneier, B., Quisquater, J.-J. (eds.) CARDIS 1998. LNCS, vol.\u00a01820, Springer, Heidelberg (2000)"},{"key":"4_CR18","volume-title":"Object-Oriented Construction","author":"B. Meyer","year":"1988","unstructured":"Meyer, B.: Object-Oriented Construction. Prentice-Hall, Englewood Cliffs (1988)"},{"issue":"6","key":"4_CR19","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/BF00277386","volume":"27","author":"C. Morgan","year":"1990","unstructured":"Morgan, C., Gardiner, P.H.B.: Data Refinement by Calculation. Acta Informatica\u00a027(6), 481\u2013503 (1990)","journal-title":"Acta Informatica"},{"key":"4_CR20","unstructured":"Sun Microsystems. Java CardTM 2.2 Off-Card Verifier. Tech. report, Sun microsystems, 901 San Antonio Road, Palo Alto, CA 94303 USA (June 2002)"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P., Poetzsch-Heffer, A., Leavens, G.T.: Modular Invariants for Layered Object Structures. Science of Computer Programming (2006)","DOI":"10.1016\/j.scico.2006.03.001"},{"key":"4_CR22","volume-title":"LICS 2004","author":"D.A. Naumann","year":"2004","unstructured":"Naumann, D.A., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state. In: LICS 2004, IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"4_CR23","unstructured":"Potet, M.-L.: Sp\u00e9cifications et d\u00e9veloppements formels: Etude des aspects compositionnels dans la m\u00e9thode B. Habilitation \u00e0 \u00a0diriger des \u00a0recherches, Institut National Polytechnique de Grenoble (d\u00e9cembre 5, 2002)"},{"issue":"3","key":"4_CR24","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1023\/A:1026538301096","volume":"17","author":"D. Sabatier","year":"2000","unstructured":"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\u00a017(3), 245\u2013272 (2000)","journal-title":"Formal Methods in System Design"}],"container-title":["Lecture Notes in Computer Science","B 2007: Formal Specification and Development in B"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11955757_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:21:30Z","timestamp":1619508090000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11955757_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540687603","9783540687610"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/11955757_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}