{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T09:50:58Z","timestamp":1758707458871},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540881933"},{"type":"electronic","value":"9783540881940"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-88194-0_16","type":"book-chapter","created":{"date-parts":[[2008,10,17]],"date-time":"2008-10-17T14:56:21Z","timestamp":1224255381000},"page":"238-257","source":"Crossref","is-referenced-by-count":7,"title":["A Practical Approach to Partiality \u2013 A Proof Based Approach"],"prefix":"10.1007","author":[{"given":"Farhad","family":"Mehta","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"Rigorous Open Development Environment for Complex Systems (RODIN) official website, http:\/\/www.event-b.org\/"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book: Assigning programs to meanings. Cambridge (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"16_CR3","unstructured":"Abrial, J.-R.: Modeling in Event B: System and Softtware Design. Cambridge (to appear, 2007)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/3-540-45648-1_13","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"J.-R. Abrial","year":"2002","unstructured":"Abrial, J.-R., Mussat, L.: On using conditional definitions in formal theories. In: Bert, D., Bowen, J., Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 242\u2013269. Springer, Heidelberg (2002)"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pp. 49\u201369 (2005)","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"16_CR6","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/BF00264250","volume":"21","author":"H. Barringer","year":"1984","unstructured":"Barringer, H., Cheng, J.H., Jones, C.B.: A logic covering undefinedness in program proofs. Acta Inf.\u00a021, 251\u2013269 (1984)","journal-title":"Acta Inf."},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/BFb0053354","volume-title":"B\u201998: Recent Advances in the Development and Use of the B Method","author":"P. Behm","year":"1998","unstructured":"Behm, P., Burdy, L., Meynadier, J.-M.: Well defined B. In: Bert, D. (ed.) B 1998. LNCS, vol.\u00a01393, pp. 29\u201345. Springer, Heidelberg (1998)"},{"key":"16_CR8","unstructured":"Berezin, S., Barrett, C., Shikanian, I., Chechik, M., Gurfinkel, A., Dill, D.L.: A practical approach to partial functions in CVC Lite"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Chalin, P.: Logical foundations of program assertions: What do practitioners want? In: SEFM, pp. 383\u2013393 (2005)","DOI":"10.1109\/SEFM.2005.26"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"International Joint Conference on Automated Reasoning (IJCAR)","author":"\u00c1. Darvas","year":"2008","unstructured":"Darvas, \u00c1., Mehta, F., Rudich, A.: Efficient well-definedness checking. In: International Joint Conference on Automated Reasoning (IJCAR). LNCS. Springer, Heidelberg (to appear, 2008)"},{"key":"16_CR11","unstructured":"Fitzgerald, J.S., Jones, C.B.: The connection between two ways of reasoning about partial functions. Technical Report CS-TR-1044, School of Computing Science. Newcastle University (August 2007)"},{"key":"16_CR12","volume-title":"Introduction to HOL: a theorem proving environment for higher order logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, New York (1993)"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/BFb0015254","volume-title":"Computer Science Today","author":"D. Gries","year":"1995","unstructured":"Gries, D., Schneider, F.B.: Avoiding the undefined by underspecification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol.\u00a01000, pp. 366\u2013373. Springer, Heidelberg (1995)"},{"key":"16_CR14","volume-title":"Systematic software development using VDM","author":"C.B. Jones","year":"1990","unstructured":"Jones, C.B.: Systematic software development using VDM, 2nd edn. Prentice-Hall, Inc., Englewood Cliffs (1990)","edition":"2"},{"key":"16_CR15","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2005.10.002","volume":"145","author":"C.B. Jones","year":"2006","unstructured":"Jones, C.B.: Reasoning about partial functions in the formal development of programs. Electr. Notes Theor. Comput. Sci.\u00a0145, 3\u201325 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"16_CR16","series-title":"Bibl. Matematica","volume-title":"Introduction to metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"Kleene, S.C.: Introduction to metamathematics. Bibl. Matematica. North-Holland, Amsterdam (1952)"},{"key":"16_CR17","unstructured":"Mehta, F.D.: Proofs for the Working Engineer. PhD thesis, ETH Zurich (2008)"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"16_CR19","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system, January\u00a015 (2001)"},{"key":"16_CR20","unstructured":"Owre, S., Shankar, N.: The formal semantics of PVS (March 1999), http:\/\/www.csl.sri.com\/papers\/csl-97-2\/"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods (FM)","author":"A. Rudich","year":"2008","unstructured":"Rudich, A., Darvas, \u00c1., M\u00fcller, P.: Checking well-formedness of pure-method specifications. In: Formal Methods (FM). LNCS. Springer, Heidelberg (2008)"},{"issue":"2","key":"16_CR22","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The TPTP (Thousands of Problems for Theorem Provers) Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88194-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T19:08:03Z","timestamp":1557860883000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88194-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540881933","9783540881940"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88194-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}