{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T00:47:14Z","timestamp":1742950034333,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540402534"},{"type":"electronic","value":"9783540448808"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44880-2_27","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:12:53Z","timestamp":1183479173000},"page":"457-476","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Formal Derivation of Spanning Trees Algorithms"],"prefix":"10.1007","author":[{"given":"Jean-Raymond","family":"Abrial","sequence":"first","affiliation":[]},{"given":"Dominique","family":"Cansell","sequence":"additional","affiliation":[]},{"given":"Dominique","family":"M\u00e9ry","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,5,27]]},"reference":[{"key":"27_CR1","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Mathematics for Program Construction","author":"J.-R. Abrial","year":"1989","unstructured":"J.-R. Abrial. A formal approach to large software constructions. In J. L. A van de Snepscheut, editor, Mathematics for Program Construction, pages 1\u201320. Springer-Verlag, june 1989. LNCS 375."},{"key":"27_CR2","unstructured":"J.-R. Abrial. Extending B without changing it (for developing distributed systems). In H. Habrias, editor, 1\n \n st\n \n Conference on the B method, pages 169\u2013190, November 1996."},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"J.-R. Abrial, D. Cansell, and D. M\u00e9ry. A mechanically proved and incremental development of the IEEE 1394 Tree Identify Protocol. Formal Aspects of Computing, ??(??), 2002. accepted for publication.","DOI":"10.1007\/s001650300002"},{"key":"27_CR4","series-title":"Lect Notes Comput Sci","volume-title":"B\u2019 98: Recent Advances in the Development and Use of the B Method","author":"J.-R. Abrial","year":"1998","unstructured":"J.-R. Abrial and L. Mussat. Introducing dynamic constraints in B. In D. Bert, editor, B\u2019 98: Recent Advances in the Development and Use of the B Method, volume 1393 of Lecture Notes in Computer Science. Springer-Verlag, 1998."},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"J.R. Abrial. The B Book \u2014 Assigning Programs to Meanings. Cambridge University Press, 1996. ISBN 0-521-49619-5.","DOI":"10.1017\/CBO9780511624162"},{"issue":"1","key":"27_CR6","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0022-0000(81)90005-2","volume":"23","author":"R. J. R. Back","year":"1979","unstructured":"R. J. R. Back. On correct refinement of programs. Journal of Computer and System Sciences, 23(1): 49\u201368, 1979.","journal-title":"Journal of Computer and System Sciences"},{"key":"27_CR7","series-title":"Lect Notes Comput Sci","volume-title":"ZB 2002","author":"D. Cansell","year":"2002","unstructured":"Dominique Cansell, Ganesh Gopalakrishnan, Mike Jones, Dominique M\u00e9ry, and Airy Weinzoepflen. Incremental proof of the producer\/consumer property for the pci protocol. In D. Bert, editor, ZB 2002, Lecture Notes in Computer Science. Springer-Verlag, January 2002."},{"key":"27_CR8","unstructured":"Dominique Cansell and Dominique M\u00e9ry. D\u00e9veloppement de fonctions d\u00e9finies r\u00e9cursivement en b. Technical report, LORIA, 2002."},{"key":"27_CR9","unstructured":"K. M. Chandy and J. Misra. Parallel Program Design A Foundation. Addison-Wesley Publishing Company, 1988. ISBN 0-201-05866-9."},{"key":"27_CR10","unstructured":"ClearSy, Aix-en-Provence (F). Atelier B, 2002. Version 3.6."},{"key":"27_CR11","unstructured":"Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Cliff Stein. Introduction to Algorithms. MIT Press and McGraw-Hill, 2001."},{"key":"27_CR12","unstructured":"E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"27_CR13","unstructured":"R. Fraer. Formal Development in B of a Minimum Spanning Tree Algorithm. In H. Habrias, editor, 1\n \n st\n \n Conference on the B method, pages 169\u2013190, November 1996."},{"key":"27_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0167-6423(93)90007-C","volume":"21","author":"E. Pascal Gribomont","year":"1993","unstructured":"E. Pascal Gribomont. Concurrency without toil: a systematic method for parallel program design. Science of Computer Programming, 21:1\u201356, 1993.","journal-title":"Science of Computer Programming"},{"key":"27_CR15","unstructured":"Y. Gurevitch. Specification and Validation Methods, chapter \u201cEvolving Algebras 1993: Lipari Guide\u201d, pages 9\u201336. Oxford University Press, 1995. Ed. E. B\u00f6rger."},{"key":"27_CR16","doi-asserted-by":"publisher","first-page":"48","DOI":"10.2307\/2033241","volume":"7","author":"J. B. Kruskal","year":"1956","unstructured":"J. B. Kruskal. On the shortest spanning subtree and the traveling salesman problem. Proc. Am. Math. Soc., 7:48\u201350, 1956.","journal-title":"Proc. Am. Math. Soc."},{"issue":"3","key":"27_CR17","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"L. Lamport. A temporal logic of actions. Transactions On Programming Languages and Systems, 16(3): 872\u2013923, May 1994.","journal-title":"Transactions On Programming Languages and Systems"},{"key":"27_CR18","unstructured":"Leslie Lamport. Specifying Systems: The TLA + Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002."},{"key":"27_CR19","unstructured":"C. Morgan. Programming from Specifications. Prentice Hall International Series in Computer Science. Prentice Hall, 1990."},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"R. C. Prim. Shortest connection and some generalizations. Bell Syst. Tech. J., 36, 1957.","DOI":"10.1002\/j.1538-7305.1957.tb01515.x"},{"issue":"4","key":"27_CR21","first-page":"304","volume":"3","author":"K. Stroetmann","year":"1997","unstructured":"K. Stroetmann. The constrained shortest path problem: A case study in using ASMs. J. of Universal Computer Science, 3(4):304\u2013319, 1997.","journal-title":"J. of Universal Computer Science"}],"container-title":["Lecture Notes in Computer Science","ZB 2003: Formal Specification and Development in Z and B"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44880-2_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,23]],"date-time":"2023-01-23T20:28:04Z","timestamp":1674505684000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44880-2_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540402534","9783540448808"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-44880-2_27","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"27 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}