{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:23:41Z","timestamp":1725456221089},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540627814"},{"type":"electronic","value":"9783540685173"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0030623","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:10:41Z","timestamp":1133417441000},"page":"520-534","source":"Crossref","is-referenced-by-count":3,"title":["Protective interface specifications"],"prefix":"10.1007","author":[{"given":"Gary T.","family":"Leavens","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeannette M.","family":"Wing","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,20]]},"reference":[{"key":"42_CR1","unstructured":"D. Andrews et al. Information technology programming languages \u2014 VDM-SL: First committee draft standard CD1387-1. Document ISO\/IEC JTC1\/SC22\/WG19 N-20, International Standards Organization, Nov. 1993. ftp:\/\/gatekeeper.dec.com\/pub\/standards\/vdmsl\/."},{"issue":"3","key":"42_CR2","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/BF00264250","volume":"21","author":"H. Barringer","year":"1984","unstructured":"H. Barringer, J. H. Cheng, and C. B. Jones. A logic covering undefinedness in program proofs. Acta Informatica, 21(3):251\u2013269, Oct. 1984.","journal-title":"Acta Informatica"},{"key":"42_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-2033-9","volume-title":"Proof in VDM: A Practitioner's Guide","author":"J. Bicarregui","year":"1994","unstructured":"J. Bicarregui, J. S. Fitgerald, P. A. Lindsay, R. Moore, and B. Ritchie. Proof in VDM: A Practitioner's Guide. Springer-Verlag, New York, N.Y., 1994."},{"key":"42_CR4","doi-asserted-by":"crossref","unstructured":"A. Bijlsma. Semantics of quasi-boolean expressions. In W. H. J. Feijen et al., editors, Beauty is Our Business, pages 27\u201335. Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4612-4476-9_4"},{"key":"42_CR5","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/BF00261259","volume":"16","author":"A. Blikle","year":"1981","unstructured":"A. Blikle. The clean termination of iterative programs. Acta Informatica, 16:199\u2013217, 1981.","journal-title":"Acta Informatica"},{"key":"42_CR6","doi-asserted-by":"crossref","first-page":"387","DOI":"10.3233\/FI-1991-14402","volume":"XIV","author":"A. Blikle","year":"1991","unstructured":"A. Blikle. Three-valued predicates for software specification and validation. Fundamenta Informaticae, XIV:387\u2013410, 1991.","journal-title":"Fundamenta Informaticae"},{"issue":"1","key":"42_CR7","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/BF00625280","volume":"18","author":"M. Broy","year":"1982","unstructured":"M. Broy and M. Wirsing. Partial abstract types. Acta Informatica, 18(1):47\u201364, Nov. 1982.","journal-title":"Acta Informatica"},{"key":"42_CR8","series-title":"Workshops in Computing Series","first-page":"51","volume-title":"On the usability of logics which handle partial functions","author":"J. H. Cheng","year":"1990","unstructured":"J. H. Cheng and C. B. Jones. On the usability of logics which handle partial functions. In C. Morgan and J. C. P. Woodcock, editors, Proceedings of the Third Refinement Workshop, Workshops in Computing Series, pages 51\u201369, Berlin, 1990. Springer-Verlag."},{"key":"42_CR9","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/BF00289066","volume":"11","author":"D. Coleman","year":"1979","unstructured":"D. Coleman and J. W. Hughes. The clean termination of Pascal programs. Acta Informatica, 11:195\u2013210, 1979.","journal-title":"Acta Informatica"},{"key":"42_CR10","volume-title":"volume 35 of Cambridge Tracts in Theoretical Computer Science","author":"L. M. G. Feijs","year":"1992","unstructured":"L. M. G. Feijs and H. B. M. Jonkers. Formal Specification and Design, volume 35 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, UK, 1992."},{"issue":"6","key":"42_CR11","doi-asserted-by":"publisher","first-page":"1044","DOI":"10.1109\/32.58789","volume":"16","author":"S. J. Garland","year":"1990","unstructured":"S. J. Garland, J. V. Guttag, and J. J. Horning. Debugging Larch Shared Language specifications. IEEE Transactions on Software Engineering, 16(6):1044\u20131057, Sept. 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"42_CR12","doi-asserted-by":"crossref","unstructured":"S. M. German. Automating proofs of the absence of common runtime errors. In Conference record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 105\u2013118. ACM, Jan. 1978.","DOI":"10.1145\/512760.512772"},{"key":"42_CR13","series-title":"number 1000 in Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/BFb0015254","volume-title":"Computer Science Today: Recent Trends and Developments","author":"D. Gries","year":"1995","unstructured":"D. Gries and F. B. Schneider. Avoiding the undefined by underspecification. In J. van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, number 1000 in Lecture Notes in Computer Science, pages 366\u2013373. Springer-Verlag, New York, N.Y., 1995."},{"key":"42_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2704-5","volume-title":"Larch: Languages and Tools for Formal Specification","author":"J. V. Guttag","year":"1993","unstructured":"J. V. Guttag, J. J. Horning, S. Garland, K. Jones, A. Modet, and J. Wing. Larch: Languages and Tools for Formal Specification. Springer-Verlag, New York, N.Y., 1993."},{"key":"42_CR15","volume-title":"Technical Report 58","author":"J. V. Guttag","year":"1990","unstructured":"J. V. Guttag, J. J. Horning, and A. Modet. Report on the Larch Shared Language: Version 2.3. Technical Report 58, Digital Equipment Corporation, Systems Research Center, 130 Lytton Avenue, Palo Alto, CA 94301, Apr. 1990. Order from src-report@src.dec.com."},{"key":"42_CR16","unstructured":"I. Hayes, editor. Specification Case Studies. International Series in Computer Science. Prentice-Hall, Inc., second edition, 1993."},{"issue":"2","key":"42_CR17","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/0020-0190(95)00042-B","volume":"54","author":"C. Jones","year":"1995","unstructured":"C. Jones. Partial functions and logics: A warning. Inf. Process. Lett., 54(2):65\u201367, 1995.","journal-title":"Inf. Process. Lett."},{"key":"42_CR18","series-title":"International Series in Computer Science","volume-title":"Systematic Software Development Using VDM","author":"C. B. Jones","year":"1990","unstructured":"C. B. Jones. Systematic Software Development Using VDM. International Series in Computer Science. Prentice Hall, Englewood Cliffs, N.J., second edition, 1990.","edition":"second edition"},{"issue":"5","key":"42_CR19","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/BF01178666","volume":"31","author":"C. B. Jones","year":"1994","unstructured":"C. B. Jones and K. Middelburg. A typed logic of partial functions reconstructed classically. Acta Informatica, 31(5):399\u2013430, 1994.","journal-title":"Acta Informatica"},{"key":"42_CR20","doi-asserted-by":"crossref","first-page":"411","DOI":"10.3233\/FI-1991-14403","volume":"XIV","author":"B. Konikowska","year":"1991","unstructured":"B. Konikowska, A. Tarlecki, and A. Blikle. A three-valued logic for software specification and validation. Fundamenta Informaticae, XIV:411\u2013453, 1991.","journal-title":"Fundamenta Informaticae"},{"key":"42_CR21","unstructured":"G. T. Leavens. Larch\/C++ Reference Manual. Version 4.20. Available in ftp:\/\/ftp.cs.iastate.edu\/pub\/larchc++\/lcpp.ps.gz or on the world wide web at the URL http:\/\/www.cs.iastate.edu\/~leavens\/larchc++.html, Dec. 1996."},{"key":"42_CR22","volume-title":"Object-oriented Software Construction","author":"B. Meyer","year":"1988","unstructured":"B. Meyer. Object-oriented Software Construction. Prentice Hall, New York, N.Y., 1988."},{"issue":"4","key":"42_CR23","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/190679.190681","volume":"19","author":"W. F. Ogden","year":"1994","unstructured":"W. F. Ogden, M. Sitaraman, B. W. Weide, and S. H. Zweben. Part I: The RESOLVE framework and discipline \u2014 a research synopsis. ACM SIGSOFT Software Engineering Notes, 19(4):23\u201328, Oct 1994.","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"issue":"2","key":"42_CR24","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for faulttolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, Feb. 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"42_CR25","series-title":"International Series in Computer Science","volume-title":"The Z Notation: A Reference Manual","author":"J. M. Spivey","year":"1992","unstructured":"J. M. Spivey. The Z Notation: A Reference Manual. International Series in Computer Science. Prentice-Hall, New York, N.Y., second edition, 1992.","edition":"second edition"},{"key":"42_CR26","unstructured":"D. S. Stefan Kahrs and A. Tarlecki. The definition of Extended ML: a gentle introduction. Technical Report ECS-LFCS-95-322, Laboratory for Foundations of Computer Science, University of Edinburgh, Oct. 1995. To appear in Theoretical Computer Science."},{"key":"42_CR27","unstructured":"J. M. Wing. A two-tiered approach to specifying programs. Technical Report TR-299, Massachusetts Institute of Technology, Laboratory for Computer Science, 1983."},{"key":"42_CR28","series-title":"volume 1009 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BFb0015461","volume-title":"KORSO: Methods, Languages and Tools for the Construction of Correct Software","author":"U. Wolter","year":"1995","unstructured":"U. Wolter, K. Didrich, F. Cornelius,; M. Klar, R. Wess\u00e4ly, and H. Ehrig. How to cope with the Spectrum of spectrum. In M. Broy and S. J\u00e4hnichen, editors, KORSO: Methods, Languages and Tools for the Construction of Correct Software, volume 1009 of Lecture Notes in Computer Science, pages 173\u2013189. Springer-Verlag, New York, N.Y., 1995."},{"key":"42_CR29","unstructured":"J. Woodcock and D. Jackson. About the semantics of partial functions in Z. Personal communication, Apr. 1996."}],"container-title":["Lecture Notes in Computer Science","TAPSOFT '97: Theory and Practice of Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0030623","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,20]],"date-time":"2021-07-20T20:18:26Z","timestamp":1626812306000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0030623"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540627814","9783540685173"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/bfb0030623","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}