{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T15:47:47Z","timestamp":1762271267257},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540682356"},{"type":"electronic","value":"9783540682370"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-68237-0_7","type":"book-chapter","created":{"date-parts":[[2008,6,4]],"date-time":"2008-06-04T05:36:00Z","timestamp":1212557760000},"page":"68-83","source":"Crossref","is-referenced-by-count":20,"title":["Checking Well-Formedness of Pure-Method Specifications"],"prefix":"10.1007","author":[{"given":"Arsenii","family":"Rudich","sequence":"first","affiliation":[]},{"given":"\u00c1d\u00e1m","family":"Darvas","sequence":"additional","affiliation":[]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book: Assigning Programs to Meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"7_CR3","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 Informatica\u00a021, 251\u2013269 (1984)","journal-title":"Acta Informatica"},{"key":"7_CR4","first-page":"29","volume-title":"International B Conference","author":"P. Behm","year":"1998","unstructured":"Behm, P., Burdy, L., Meynadier, J.-M.: Well Defined B. In: International B Conference, pp. 29\u201345. Springer-Verlag, Heidelberg (1998)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Berezin, S., Barrett, C., Shikanian, I., Chechik, M., Gurfinkel, A., Dill, D.L.: A practical approach to partial functions in CVC Lite. In: PDPAR (2004)","DOI":"10.1016\/j.entcs.2004.06.064"},{"key":"7_CR6","volume-title":"Texts in Theoretical Computer Science","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. In: Texts in Theoretical Computer Science, Springer, Heidelberg (2004)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"422","DOI":"10.1007\/978-3-540-45236-2_24","volume-title":"FME 2003: Formal Methods","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Requet, A., Lanet, J.-L.: Java applet correctness: A developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 422\u2013439. Springer, Heidelberg (2003)"},{"issue":"2","key":"7_CR8","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/s00165-006-0016-1","volume":"19","author":"P. Chalin","year":"2007","unstructured":"Chalin, P.: Are the logical foundations of verifying compiler prototypes matching user expectations? Formal Aspects of Computing\u00a019(2), 139\u2013158 (2007)","journal-title":"Formal Aspects of Computing"},{"key":"7_CR9","first-page":"23","volume-title":"ICSE","author":"P. Chalin","year":"2007","unstructured":"Chalin, P.: A sound assertion semantics for the dependable systems evolution verifying compiler. In: ICSE, pp. 23\u201333. IEEE Computer Society Press, Los Alamitos (2007)"},{"issue":"8","key":"7_CR10","doi-asserted-by":"crossref","first-page":"77","DOI":"10.5381\/jot.2005.4.8.a4","volume":"4","author":"D. Cok","year":"2005","unstructured":"Cok, D.: Reasoning with specifications containing method calls and model fields. Journal of Object Technology\u00a04(8), 77\u2013103 (2005)","journal-title":"Journal of Object Technology"},{"key":"7_CR11","unstructured":"Crow, J., Owre, S., Rushby, J., Shankar, N., Srivas, M.: A Tutorial Introduction to PVS (April 1995)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-540-71289-3_26","volume-title":"Fundamental Approaches to Software Engineering","author":"\u00c1. Darvas","year":"2007","unstructured":"Darvas, \u00c1., Leino, K.R.M.: Practical reasoning about invocations and implementations of pure methods. In: Dwyer, M.B., Lopes, A. (eds.) FASE 2007. LNCS, vol.\u00a04422, pp. 336\u2013351. Springer, Heidelberg (2007)"},{"issue":"5","key":"7_CR13","doi-asserted-by":"crossref","first-page":"59","DOI":"10.5381\/jot.2006.5.5.a3","volume":"5","author":"\u00c1. Darvas","year":"2006","unstructured":"Darvas, \u00c1., M\u00fcller, P.: Reasoning About Method Calls in Interface Specifications. Journal of Object Technology (JOT)\u00a05(5), 59\u201385 (2006)","journal-title":"Journal of Object Technology (JOT)"},{"key":"7_CR14","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (2003)"},{"key":"7_CR15","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":"7_CR16","unstructured":"Hall, J.G., McDermid, J.A., Toyn, I.: Model conjectures for Z specifications. In: 7th International Conference on Putting into Practice Methods and Tools for Information System Design, pp. 41\u201351 (1995)"},{"key":"7_CR17","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1002\/malq.19790251304","volume":"25","author":"A. Hoogewijs","year":"1979","unstructured":"Hoogewijs, A.: On a formalization of the non-definedness notion. Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik\u00a025, 213\u2013217 (1979)","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik"},{"key":"7_CR18","volume-title":"Systematic software development using VDM","author":"C.B. Jones","year":"1986","unstructured":"Jones, C.B.: Systematic software development using VDM. Prentice-Hall, Englewood Cliffs (1986)"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","first-page":"108","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"J.R. Kiniry","year":"2005","unstructured":"Kiniry, J.R., Cok, D.R.: ESC\/Java2: Uniting ESC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"7_CR20","unstructured":"Kleene, S.C.: Introduction to Metamathematics. Van Nostrand (1952)"},{"issue":"3","key":"7_CR21","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\u00a031(3), 1\u201338 (2006)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"7_CR23","unstructured":"Rudich, A., Darvas, \u00c1., M\u00fcller, P.: Checking well-formedness of pure-method specifications (Full Paper). Technical Report 588, ETH Zurich (2008)"},{"issue":"9","key":"7_CR24","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"J. Rushby","year":"1998","unstructured":"Rushby, J., Owre, S., Shankar, N.: Subtypes for Specifications: Predicate Subtyping in PVS. IEEE Transactions on Software Engineering\u00a024(9), 709\u2013720 (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR25","volume-title":"Understanding Z: a specification language and its formal semantics","author":"J.M. Spivey","year":"1988","unstructured":"Spivey, J.M.: Understanding Z: a specification language and its formal semantics. Cambridge University Press, Cambridge (1988)"},{"key":"7_CR26","first-page":"233","volume-title":"International Conference of Z Users","author":"S.H. Valentine","year":"1998","unstructured":"Valentine, S.H.: Inconsistency and Undefinedness in Z - A Practical Guide. In: International Conference of Z Users, pp. 233\u2013249. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","FM 2008: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68237-0_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:43:47Z","timestamp":1620017027000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68237-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540682356","9783540682370"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68237-0_7","relation":{},"subject":[]}}