{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:09:57Z","timestamp":1775052597910,"version":"3.50.1"},"reference-count":26,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2001,10,1]],"date-time":"2001-10-01T00:00:00Z","timestamp":1001894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2014,11,20]],"date-time":"2014-11-20T00:00:00Z","timestamp":1416441600000},"content-version":"vor","delay-in-days":4798,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2001,10]]},"DOI":"10.1016\/s1571-0661(04)00247-6","type":"journal-article","created":{"date-parts":[[2004,1,29]],"date-time":"2004-01-29T10:14:39Z","timestamp":1075371279000},"page":"103-117","source":"Crossref","is-referenced-by-count":52,"title":["Jass \u2014 Java with Assertions1 1This work was partially funded by the German Research Council (DFG) under grant OL 98\/3-1."],"prefix":"10.1016","volume":"55","author":[{"given":"Detlef","family":"Bartetzko","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clemens","family":"Fischer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"M\u00f6ller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB1","doi-asserted-by":"crossref","unstructured":"America, P., Designing an object-oriented programming language with behavioural subtyping, in: J. de Bakker, W. de Roever and G. Rozenberg, editors, REX Workshop: Foundations of Object-Oriented Languages, number 489 in LNCS (1991)","DOI":"10.1007\/BFb0019440"},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB2","series-title":"\u201cVerification of Sequential and Concurrent Programs,\u201d","author":"Apt","year":"1997"},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB3","unstructured":"Bartetzko D., \u201cParallelit\u00e4t und Vererbung beim \u201cProgrammieren mit Vertrag\u201d,\u201d Master's thesis, Universit\u00e4t Oldenburg (1999), in German."},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB4","doi-asserted-by":"crossref","unstructured":"Clarke E., E. Emerson and A. Sistla, Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach, in: Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, ACM, 1983, pp. 117\u2013126.","DOI":"10.1145\/567067.567080"},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB5","unstructured":"Corbett J., M. Dwyer, J. Hatcliff and Robby, A language framework for expressing checkable properties of dynamic software, in: SPIN 2000, number 1885 in LNCS (2000), pp. 205\u2013223."},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB6","series-title":"\u201cData Refinement \u2013 Model-Oriented Proof Methods and their Comparison,\u201d","author":"de Roever","year":"1998"},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB7","unstructured":"Detlefs D., R. Leino, G. Nelson and J. Saxe, Extended static checking, Technical Report 159, Compaq Systems Research Center (1998)."},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB8","doi-asserted-by":"crossref","unstructured":"Dhara, K. K. and G. T. Leavens, Forcing behavioral subtyping through specification inheritance, in: Proceedings of the 18th International Conference on Software Engineering, Berlin, Germany (1996), pp. 258\u2013267.","DOI":"10.1109\/ICSE.1996.493421"},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB9","series-title":"Formal Methods for Open Object-Based Distributed Systems (FMOODS '97)","first-page":"423","article-title":"CSP-OZ: A combination of Object-Z and CSP","author":"Fischer","year":"1997"},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB10","unstructured":"Fischer C., \u201cCombination and Implementation of Processes and Data: From CSP-OZ to Java,\u201d Ph.D. thesis, University of Oldenburg (2000)."},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB11","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Comm. of the ACM"},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB12","series-title":"\u201cCommunicating Sequential Processes,\u201d","author":"Hoare","year":"1985"},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB13","series-title":"\u201cDesign and Validation of Computer Protocols,\u201d","author":"Holzmann","year":"1990"},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB14","doi-asserted-by":"crossref","unstructured":"Huisman M. and B. Jacobs, Java program verification via a Hoare logic with abrupt termination, in: T. Maibaum, editor, FASE 2000: Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science 1783 (2000), pp. 284\u2013303.","DOI":"10.1007\/3-540-46428-X_20"},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB15","unstructured":"Huzing K., R. Kuuiper and SOOP, Verification of object-oriented programs using class invariants, in: T. Maibaum, editor, FASE 2000: Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science 1783 (2000), pp. 208\u2013221."},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB16","doi-asserted-by":"crossref","unstructured":"Kramer R., iContract - the Java Design by Contract tool, Technical report, Reliable Systems (1998), http:\/\/www.reliable-systems.com.","DOI":"10.1109\/TOOLS.1998.711021"},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB17","unstructured":"Leavens G., A. Baker and C. Ruby, Preliminary design of JML: A behavioral interface specification language for java, Technical report, Department of Computer Science, Iowa State University (1998, revised 2001)."},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB18","doi-asserted-by":"crossref","first-page":"1811","DOI":"10.1145\/197320.197383","article-title":"A behavioural notion of subtyping","volume":"16","author":"Liskov","year":"1994","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB19","doi-asserted-by":"crossref","unstructured":"Luckham D., F. von Henke, B. Krieg-Br\u00fcckner and O. Owe, \u201cANNA - A language for annotating Ada programs,\u201d Lecture Notes in Computer Science 260, Springer, 1987.","DOI":"10.1007\/3-540-17980-1"},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB20","unstructured":"Meemken D., \u201cProgrammieren mit Vertrag in Java,\u201d Master's thesis, Universit\u00e4t Oldenburg (1997), in German."},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB21","series-title":"\u201cObject-Oriented Software Construction,\u201d","author":"Meyer","year":"1997"},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB22","series-title":"Foundations of Component-Based Systems","article-title":"Modular specification and verification techniques for object-oriented software components","author":"M\u00fcller","year":"2000"},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB23","unstructured":"Plath M., \u201cTrace Zusicherungen in Jass - Erweiterung des Konzepts \u201cProgrammieren mit Vertrag\u201d,\u201d Master's thesis, Universit\u00e4t Oldenburg (2000), in German."},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB24","unstructured":"Sun Microsystems, A simple assertions facility for the Java programming language, http:\/\/jcp.org\/jsr\/detail\/41.jsp."},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB25","doi-asserted-by":"crossref","unstructured":"Visser W., G. Brat, K. Havelund and S. Park, Model checking programs, in: International Conference on Automated Software Engineering, 2000.","DOI":"10.1109\/ASE.2000.873645"},{"key":"10.1016\/S1571-0661(04)00247-6_NEWBIB26","series-title":"\u201cUsing Z: Specification, Refinement, and Proof,\u201d","author":"Woodcock","year":"1996"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104002476?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104002476?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,15]],"date-time":"2019-02-15T09:54:18Z","timestamp":1550224458000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104002476"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,10]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2001,10]]}},"alternative-id":["S1571066104002476"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00247-6","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2001,10]]}}}