{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,25]],"date-time":"2026-09-25T00:51:49Z","timestamp":1790297509793,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540679448","type":"print"},{"value":"9783540445258","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44525-0_8","type":"book-chapter","created":{"date-parts":[[2007,5,1]],"date-time":"2007-05-01T10:00:58Z","timestamp":1178013658000},"page":"107-126","source":"Crossref","is-referenced-by-count":5,"title":["Compositional Structuring in the B-Method: A Logical Viewpoint of the Static Context"],"prefix":"10.1007","author":[{"given":"Theo","family":"Dimitrakos","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Juan","family":"Bicarregui","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Brian","family":"Matthews","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tom","family":"Maibaum","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2000,12,21]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"J.R. Abrial. The B-Book: Assigning Programs to Meanings. C.U.P., 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"8_CR2","unstructured":"B-CORE (UK) Ltd. The b-toolkit. 1999. URL: http:\/\/www.b-core.com ."},{"issue":"1","key":"8_CR3","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1093\/jigpal\/3.1.7","volume":"3","author":"J. Barwise","year":"1995","unstructured":"J. Barwise, D. Gabbay, and C. Hartonas. On the logic of information flow. Bulletin Of The IGPL, 3(1):7\u201349, 1995.","journal-title":"Bulletin Of The IGPL"},{"key":"8_CR4","unstructured":"D. Bert, M-L. Potet, and Y. Rouzaud. A study on Components and Assembly primitives in B. In H. Habrias, ed., First Conference on the B-Method, 1996."},{"key":"8_CR5","unstructured":"J.C. Bicarregui. Non-Interference, Security and Bisimulation: explorations into the roles of Read and Write frames. CLRC-RAL, 1998."},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"J.C. Bicarregui and et al. Formal Methods Into Practice: case studies in the application of the B Method. I.E.E. Transactions on Software Engineering, 1997.","DOI":"10.1049\/ip-sen:19970974"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"J.C. Bicarregui, J. Dick, B. Matthews, and E. Woods. Making the most of formal specification through animation, testing and proof. Sci. of Comp. Prog., 1997.","DOI":"10.1016\/S0167-6423(96)00029-9"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"J. van Benthem. Modality, bisimulation and interpolation in infinitary logic. ANNALSPAL: Annals of Pure and Applied Logic, 96, 1999.","DOI":"10.1016\/S0168-0072(98)00029-3"},{"key":"8_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/3-540-48119-2_25","volume-title":"FM\u201999-Formal Methods","author":"M. Buchi","year":"1999","unstructured":"M. Buchi and B. Back. Compositional Symmetric Sharing in B. In FM\u201999-Formal Methods, volume I of LNCS, pages 431\u2013451. Springer, Septermber 1999."},{"key":"8_CR10","unstructured":"D. Clutterbuck, J.C. Bicarregui, and B.M. Matthews. Experiences with proof in formal development. In H. Habrias, ed., First Conference on the B-Method, 1996."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"W. Craig. Three uses of the Herbrand-Getzen theorem in relating model theory and proof theory. Journal of Symbolic Logic XXII, pages 269\u2013285, 1957.","DOI":"10.2307\/2963594"},{"key":"8_CR12","series-title":"Lect Notes Comput Sci","volume-title":"STACS 95","author":"G. Dagostino","year":"1995","unstructured":"G. D\u2019Agostino, A. Montanari, and A. Policriti. A set-theoretic translation method for (poly)modal logics. Lecture Notes in Computer Science 900, 1995."},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Th. Dimitrakos and T.S.E. Maibaum. Notes on refinement, interpolation and uniformity. In ASE\u201997, 12th IEEE Int. Conf., 1997.","DOI":"10.1109\/ASE.1997.632830"},{"key":"8_CR14","unstructured":"Theodosis Dimitrakos. Formal support for specification design and implementation. PhD thesis, Imperial College, March 1998."},{"key":"8_CR15","unstructured":"Theodosis Dimitrakos. Parameterising specifications on diagrams. In ASE\u201998, 13th IEEE Int. Conf., 1998."},{"issue":"1\u20132","key":"8_CR16","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0020-0190(00)00037-5","volume":"74","author":"T. Dimitrakos","year":"2000","unstructured":"Theodosis Dimitrakos and Tom Maibaum. On a generalised modularisation theorem. Information Processing Letters, 74(1\u20132):65\u201371, 2000.","journal-title":"Information Processing Letters"},{"key":"8_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1007\/3-540-48119-2_27","volume-title":"FM\u201999-Formal Methods","author":"S. Dunne","year":"1999","unstructured":"S. Dunne. The Safe Machine: A New Specification Construct for B. In FM\u201999-Formal Methods, volume I of LNCS, pages 472\u2013489. Springer, Septermber 1999."},{"key":"8_CR18","unstructured":"H. B. Enderton. A Mathematical Introduction to Logic. Academic Press, 1972."},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Cliff B. Jones. Accomodating interference in the formal design of concurrent object-based programs. Formal Methods in System Design, 8(2):105\u2013122, March 1996.","DOI":"10.1007\/BF00122417"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Kevin Lano. The B Language and Method. Springer-Verlag, 1996.","DOI":"10.1007\/978-1-4471-1494-9"},{"key":"8_CR21","first-page":"27","volume-title":"Z User Workshop","author":"P.J. Lupton","year":"1990","unstructured":"P.J. Lupton. Promotin Forward Simulation. In J.E. Nicholls, editor, Z User Workshop, pages 27\u201349. Springer-Verlag, Oxford 1990."},{"key":"8_CR22","series-title":"Lect Notes Comput Sci","volume-title":"2nd International B Conference","author":"B. Matthews","year":"1998","unstructured":"B. Matthews, B. Ritchie, and J. Bicarregui. Synthesising structure from flat specifications. In 2nd International B Conference, LNCS, 1998."},{"key":"8_CR23","doi-asserted-by":"crossref","first-page":"579","DOI":"10.1093\/jigpal\/3.4.579","volume":"3","author":"M.C. Mere","year":"1995","unstructured":"M.C. Mere and P.A.S. Veloso. Definition-like extensions by sorts Bulletin of the IGPL, 3:579\u2013595, 1995.","journal-title":"Bulletin of the IGPL"},{"key":"8_CR24","unstructured":"B. Meyer. Object Oriented Construction. Prentice-Hall, 1988."},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"M-L. Potet and Y. Rouzaud. Composition and Refinement in the B-Method. In D. Bert, editor, Second B International Conference, pages 46\u201365, 1998.","DOI":"10.1007\/BFb0053355"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Yann Rouzaud. Interpreting the B-Method in the Refinement Calculus. In J. Wing, J. Woodcock, and J. Davies, editors, FM\u201999-Formal Methods, vol. I, 1999.","DOI":"10.1007\/3-540-48119-2_24"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"P.Y.A Ryan and S.A. Schneider. Process algebra and non-interference. In PCSFW: Proc. of The 12th Computer Security Foundations Workshop. IEEE Comp. Soc. Press, 1999.","DOI":"10.1109\/CSFW.1999.779775"},{"key":"8_CR28","unstructured":"Ketil St\u00f8len. Development of Parallel Programs on Shared Data-Structures. PhD thesis, University of Manchester, 1990. Available as a technical report UMCS-91-1-1."},{"key":"8_CR29","unstructured":"Wladyslaw M. Turski and Thomas S. E. Maibaum. The Specification of Computer Programs. Addison-Wesley, 1987."},{"key":"8_CR30","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0020-0190(94)00203-B","volume":"53","author":"P.A.S. Veloso","year":"1995","unstructured":"P.A.S. Veloso and T.S.E. Maibaum. On the modularisation theorem for logical specifications. Information Processing Letters 53, pages 287\u2013293, 1995.","journal-title":"Information Processing Letters"},{"key":"8_CR31","unstructured":"P.A.S. Veloso and S.R.M. Veloso. On extensions by function symbols: coservativeness and comparison. Tech. Report. COPPE\/UFRJ. 1990. (See also [23,32])"},{"key":"8_CR32","unstructured":"P.A.S. Veloso and S.R.M. Veloso. Some remarks on conservative extensions: a Socratic dialogue. Bulletin of the EATCS, vol. 43, 1991."},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"J.C.P. Woodcock. Mathematics as a Management Tool: Proof Rules for Promotion. In CSR Sixth Annual Conference on Large Sofware Systems. Bristol, 1989.","DOI":"10.1007\/978-94-009-0771-3_18"}],"container-title":["Lecture Notes in Computer Science","ZB 2000: Formal Specification and Development in Z and B"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44525-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T16:32:17Z","timestamp":1556382737000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44525-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540679448","9783540445258"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-44525-0_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}