{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T15:48:45Z","timestamp":1742917725021,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642151866"},{"type":"electronic","value":"9783642151873"}],"license":[{"start":{"date-parts":[[2010,9,30]],"date-time":"2010-09-30T00:00:00Z","timestamp":1285804800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2010,9,30]],"date-time":"2010-09-30T00:00:00Z","timestamp":1285804800000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-15187-3_7","type":"book-chapter","created":{"date-parts":[[2010,10,19]],"date-time":"2010-10-19T13:08:46Z","timestamp":1287493726000},"page":"115-124","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Tools and Behavioral Abstraction: A Direction for Software Engineering"],"prefix":"10.1007","author":[{"given":"K. Rustan M.","family":"Leino","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,9,30]]},"reference":[{"key":"7_CR0","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: An open toolset for modelling and reasoning in Event-B. International Journal on Software Tools for Technology Transfer (April 2010)","DOI":"10.1007\/s10009-010-0145-y"},{"key":"7_CR3","volume-title":"On the Correctness of Refinement Steps in Program Development","author":"R.-J. Back","year":"1978","unstructured":"Back, R.-J.: On the Correctness of Refinement Steps in Program Development. PhD thesis, University of Helsinki (1978) Report A-1978-4."},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer-Verlag (1998)","DOI":"10.1007\/978-1-4612-1674-2_1"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Barnett, M., F\u00a8ahndrich, M., Logozzo, F.: Embedded contract languages. In ACM SAC - OOPS. ACM (March 2010)","DOI":"10.1145\/1774088.1774531"},{"key":"7_CR6","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, and Traian Muntean, editors, CASSIS 2004, Construction and Analysis of Safe, Secure and Interoperable Smart devices, volume 3362 of Lecture Notes in Computer Science, pages 49\u201369. Springer (2005)"},{"key":"7_CR7","unstructured":"Baudin, P., Filliatre, J.-C., March\u00b4, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language, version 1.4 (2009) http:\/\/frama-c.com\/."},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/BF01933419","volume":"8","author":"E.W. Dijkstra","year":"1968","unstructured":"Dijkstra, E.W.: A constructive approach to the problem of program correctness. BIT, 8:174\u2013186 (1968)","journal-title":"BIT"},{"issue":"1","key":"7_CR9","first-page":"1","volume":"11","author":"D. Gries","year":"1990","unstructured":"Gries, D., Volpano, D.: The transform \u2014 a new language construct. Structured Programming, 11(1):1\u201310 (1990)","journal-title":"Structured Programming"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart Play-out of behavioral requirements. In Mark Aagaard and John W. O\u2019Leary, editors, Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, volume 2517 of Lecture Notes in Computer Science, pages 378\u2013398. Springer (November 2002)","DOI":"10.1007\/3-540-36126-X_23"},{"key":"7_CR11","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00a8uller, P., Parkinson, M.: Behavioral interface specification languages. Technical Report CS-TR-09-011, University of Central Florida, School of EECS (2009)"},{"issue":"4","key":"7_CR12","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, 1(4):271\u2013281 (1972)","journal-title":"Acta Informatica"},{"key":"7_CR13","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press (2006)"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Jackson, E.K., Seifert, D., Dahlweid, M., Santen, T., Bj\u00f8rner, D., Schulte, W.: Specifying and composing non-functional requirements in model-based development. In Alexandre Bergel and Johan Fabry, editors, Proceedings of the 8th International Conference on Software Composition, volume 5634 of Lecture Notes in Computer Science, pages 72\u201389. Springer (July 2009)","DOI":"10.1007\/978-3-642-02655-3_7"},{"key":"7_CR15","unstructured":"Jones, C.B.: Systematic Software Development Using VDM. International Series in Computer Science. Prentice Hall, Englewood Cliffs, N.J., second edition (1990)"},{"issue":"3","key":"7_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G.T. Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes, 31(3):1\u201338, (March 2006)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"7_CR17","unstructured":"Meyer, B.: Object-oriented Software Construction. Series in Computer Science. Prentice- Hall International (1988)"},{"key":"7_CR18","unstructured":"Microsoft: Silverlight. http:\/\/www.microsoft.com\/silverlight\/."},{"key":"7_CR19","unstructured":"Microsoft: Axum. http:\/\/msdn.microsoft.com\/en-us\/devlabs\/dd795202.aspx (2010)"},{"issue":"1","key":"7_CR20","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s10270-006-0012-1","volume":"6","author":"J. Misra","year":"2007","unstructured":"Misra, J., Cook, W.R.: Computation orchestration: A basis for wide-area computing. Software and Systems Modeling, 6(1):83\u2013110, (March 2007)","journal-title":"Software and Systems Modeling"},{"key":"7_CR21","unstructured":"Morgan, C.: Programming from Specifications. Series in Computer Science. Prentice-Hall International (1990)"},{"issue":"3","key":"7_CR22","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","volume":"9","author":"J.M. Morris","year":"1987","unstructured":"Morris, J.M.: A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9(3):287\u2013306, (December 1987)","journal-title":"Science of Computer Programming"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Schwartz, J.T., Dewar, R.B.K., Dubinsky, E., Schonberg, E.: Programming with Sets: An Introduction to SETL. Texts and Monographs in Computer Science. Springer (1986)","DOI":"10.1007\/978-1-4613-9575-1"},{"issue":"9","key":"7_CR24","doi-asserted-by":"publisher","first-page":"1024","DOI":"10.1109\/32.58788","volume":"16","author":"D.R. Smith","year":"1990","unstructured":"Smith, D.R.: KIDS: A semi-automatic program development system. IEEE Transactions on Software Engineering, 16(9):1024\u20131043, (September 1990)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"11","key":"7_CR25","doi-asserted-by":"publisher","first-page":"1278","DOI":"10.1109\/TSE.1985.231879","volume":"11","author":"D.R. Smith","year":"1985","unstructured":"Smith, D.R., Kotik, G.B., Westfold, S.J.: Research on knowledge-based software environments at Kestrel Institute. IEEE Transactions on Software Engineering, 11(11):1278\u20131295, (November 1985)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR26","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1145\/362575.362577","volume":"14","author":"N. Wirth","year":"1971","unstructured":"Wirth, N.: Program Development by Stepwise Refinement. Communications of the ACM, 14:221\u2013227 (1971)","journal-title":"Communications of the ACM"}],"container-title":["The Future of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15187-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,23]],"date-time":"2023-01-23T20:56:26Z","timestamp":1674507386000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-15187-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9,30]]},"ISBN":["9783642151866","9783642151873"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15187-3_7","relation":{},"subject":[],"published":{"date-parts":[[2010,9,30]]},"assertion":[{"value":"30 September 2010","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}