{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T19:40:02Z","timestamp":1737402002547,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540752202"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75221-9_11","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T10:33:13Z","timestamp":1188469993000},"page":"255-279","source":"Crossref","is-referenced-by-count":3,"title":["Proving Theorems About JML Classes"],"prefix":"10.1007","author":[{"given":"Leo","family":"Freitas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","volume-title":"Graduate Texts in Computer Science","author":"R.J. Back","year":"1998","unstructured":"Back, R.J., von Wright, J.: Refinement Calculus: A Systematic Introduction. In: Graduate Texts in Computer Science, Springer, Heidelberg (1998)"},{"key":"11_CR2","volume-title":"Effective Java Programming Language Guide","author":"J. Bloch","year":"2001","unstructured":"Bloch, J.: Effective Java Programming Language Guide. Prentice Hall, Englewood Cliffs (2001)"},{"issue":"3","key":"11_CR3","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. STTT\u00a07(3), 212\u2013232 (2005)","journal-title":"STTT"},{"key":"11_CR4","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)"},{"key":"11_CR5","volume-title":"12th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007)","author":"A. Butterfield","year":"2007","unstructured":"Butterfield, A., Woodcock, J.: Formalising flash memory: first steps. In: 12th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007), Auckland, New Zealand, July 11-14, 2007, IEEE Computer Press, Los Alamitos (2007)"},{"key":"11_CR6","unstructured":"Cavalcanti, A.L.C.: A Refinement Calculus for Z. DPhil Thesis. University of Oxford (1997)"},{"key":"11_CR7","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"697","DOI":"10.1007\/11901433_38","volume-title":"Formal Methods and Software Engineering","author":"L. Freitas","year":"2006","unstructured":"Freitas, L., Cavalanti, A.L.C., Woodcock, J.C.P.: Taking our own medicine: applying the refinement calculus to state-rich refinement model checking. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 697\u2013716. Springer, Heidelberg (2006)"},{"key":"11_CR9","unstructured":"Freitas, L., et\u00a0al.: Verified Software Repository @ SourceForge (2006), vsr.sourceforge.net"},{"key":"11_CR10","volume-title":"12th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007)","author":"L. Freitas","year":"2007","unstructured":"Freitas, L., Fu, Z., Woodcock, J.: POSIX file store in Z\/Eves:\u00a0an experiment in the verified software repository. In: 12th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007), Auckland, New Zealand, July 11\u201314, 2007, IEEE Computer Press, Los Alamitos (2007)"},{"key":"11_CR11","unstructured":"Fu, Z.: A Refinement of the UNIX Filing System using Z\/Eves. Master\u2019s thesis, University of York (2006)"},{"key":"11_CR12","volume-title":"The Java Language Specification","author":"J. Gosling","year":"2005","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Addison Wesley, Reading (2005)","edition":"3"},{"issue":"1","key":"11_CR13","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"T. Hoare","year":"2003","unstructured":"Hoare, T.: The Verifying Compiler Software Grand Challenge. Journal of the ACM\u00a050(1), 63\u201369 (2003)","journal-title":"Journal of the ACM"},{"key":"11_CR14","series-title":"International Series in Computer Science","volume-title":"Unifying Theories of Programming","author":"C.A.R. Hoare","year":"1998","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1998)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","first-page":"109","volume-title":"Object-Oriented Technology. ECOOP\u201999 Workshop Reader","author":"M. Huisman","year":"1999","unstructured":"Huisman, M., Jacobs, B., van den Berg, J.: A Case study in class library verification: Java\u2019s Vector class. In: Moreira, A.M.D., Demeyer, S. (eds.) Object-Oriented Technology. ECOOP\u201999 Workshop Reader. LNCS, vol.\u00a01743, pp. 109\u2013110. Springer, Heidelberg (1999)"},{"key":"11_CR16","unstructured":"Huisman, M.: Reasoning about Java Programs in Higher-Order Logic using PVS and Isabelle. PhD thesis, Universiteit Nijmegen (2001)"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/3-540-45442-X_11","volume-title":"Mathematics of Program Construction","author":"M. Huisman","year":"2002","unstructured":"Huisman, M.: Verification of Java\u2019s AbstractCollection class: a case study. In: Boiten, E.A., M\u00f6ller, B. (eds.) MPC 2002. LNCS, vol.\u00a02386, pp. 175\u2013194. Springer, Heidelberg (2002)"},{"key":"11_CR18","unstructured":"IBM: CICS Application Programming Interface Release\u00a03. Technical Report SC33-1688-01, IBM Hursley Park (1999)"},{"key":"11_CR19","unstructured":"Intel Corp.: Open NAND Flash Interface Specification. Open NAND Flash Interface Consortium (2007), http:\/\/www.onfi.org\/"},{"key":"11_CR20","unstructured":"ISO\/IEC 13568: Information Technology\u2014Z Formal Specification Notation\u2014Syntax, Type System and Semantics. First edn. ISO\/IEC (2002)"},{"key":"11_CR21","unstructured":"Josey, A. (ed.): The Single UNIX Specification Version 3. Open Group (2004), ISBN: 193162447X"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Joshi, R., Holzmann, G.J.: A mini-challenge: build a verifiable filesystem. In: Verified Software: Theories, Tools, Experiments (VSTTE), IFIP Working Conference, Zurich (in press)","DOI":"10.1007\/978-3-540-69149-5_6"},{"key":"11_CR23","volume-title":"Proofs and Refutations: The Logic of Mathematical Discovery","author":"I. Lakatos","year":"2005","unstructured":"Lakatos, I.: Proofs and Refutations: The Logic of Mathematical Discovery. Cambrdige University Press, Cambrdige (2005)"},{"key":"11_CR24","unstructured":"Leavens,\u00a0G.\u00a0T., Poll,\u00a0E., Clifton,\u00a0C., Cheon,\u00a0Y., Ruby,\u00a0C., Cok,\u00a0D., M\u00fcller,\u00a0P., Kiniry,\u00a0J., Chalin,\u00a0P.: JML Reference Manual. Iowa State University. Revision 1.200 (2007)"},{"key":"11_CR25","volume-title":"Programming from Specifications","author":"C. Morgan","year":"1994","unstructured":"Morgan, C.: Programming from Specifications. Prentice-Hall, Englewood Cliffs (1994)"},{"key":"11_CR26","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1109\/TSE.1984.5010215","volume":"SE-10","author":"C. Morgan","year":"1984","unstructured":"Morgan, C., Sufrin, B.: Specification of the UNIX filing system. IEEE Transactions on Software Engineering\u00a0SE-10, 128\u2013142 (1984)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"3","key":"11_CR27","doi-asserted-by":"crossref","first-page":"121","DOI":"10.5381\/jot.2004.3.3.a3","volume":"3","author":"R.F. Paige","year":"2004","unstructured":"Paige, R.F., Brooke, P.J.: Integrating BON and Object-Z. Journal of Object Technology\u00a03(3), 121\u2013141 (2004)","journal-title":"Journal of Object Technology"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Paige, R.F., Ostroff, J.S.: From Z to BON\/Eiffel. In: ASE, pp. 209\u2013212 (1998)","DOI":"10.1109\/ASE.1998.732645"},{"key":"11_CR29","series-title":"Bristol. IFIP Conference Proceedings","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-0-387-35528-3_8","volume-title":"Specification of the JavaCard API in JML. Smart Card Research and Advanced Applications","author":"E. Poll","year":"2000","unstructured":"Poll, E., van den Berg, J., Jacobs, B.: 3. In: Specification of the JavaCard API in JML. Smart Card Research and Advanced Applications. Proceedings of the Fourth Working Conference on Smart Card Research and Advanced Applications, CARDIS 2000, September 20-22, 2000. Bristol. IFIP Conference Proceedings, vol.\u00a0180, pp. 135\u2013154. Kluwer, Dordrecht (2000)"},{"key":"11_CR30","unstructured":"Raghavan, A.D., Leavens, G.T.: Desugaring JML Method Specifications. Technical Report TR#00-03e, Iowa State University, Department of Computer Science 226 Atanasoff Hall Ames Iowa 50011-1041, USA (2005)"},{"key":"11_CR31","unstructured":"Russell, B.: Recent Work in Philosophy of Mathematics. International Monthly (1901) Reprinted in Mysticism and Logic and Other Essays (p.59\u201374) Barnes & Noble (1976)"},{"key":"11_CR32","unstructured":"Saaltink, M.: Z\/Eves 2.0 User\u2019s Guide. ORA Canada, TR-99-5493-06a (1999)"},{"key":"11_CR33","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-5265-9","volume-title":"The Object-Z Specification Language. Advances in Formal Methods","author":"G. Smith","year":"2000","unstructured":"Smith, G.: The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"11_CR34","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"1998","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice-Hall, Englewood Cliffs (1998)"},{"key":"11_CR35","unstructured":"SRI: Workshop on the Verification Grand Challenge (2005), http:\/\/www.csl.sri.com"},{"key":"11_CR36","unstructured":"Stepney, S., Cooper, D., Woodcock, J.: An Electronic Purse:\u00a0Specification, Refinement, and Proof. Technical Monograph PRG-126, University of Oxford (2000)"},{"key":"11_CR37","unstructured":"Stepney, S., Polack, F., Toyn, I.: A Z Patterns Catalougue: volume 1. Technical Report YCS349, Department of Computer Science, University of York (2003)"},{"key":"11_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/3-540-44880-2_20","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"M. Utting","year":"2003","unstructured":"Utting, M., Wang, S.: Object orientation without extending Z. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol.\u00a02651, pp. 319\u2013338. Springer, Heidelberg (2003)"},{"key":"11_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-45165-X_11","volume-title":"Java on Smart Cards: Programming and Security","author":"J. Berg van den","year":"2001","unstructured":"van den Berg, J., Jacobs, B., Poll, E.: Formal specification and verification of JavaCard\u2019s Application Identifier class. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol.\u00a02041, pp. 137\u2013150. Springer, Heidelberg (2001)"},{"key":"11_CR40","doi-asserted-by":"crossref","unstructured":"Woodcock, J.C.P., Cavalcanti, A.L.C.: A concurrent language for refinement. In: 5th Irish Workshop on Formal Methods, IWFM 2001, Dublin, Ireland, 16\u201317 July 2001. BCS Workshops in Computing (2001)","DOI":"10.14236\/ewic\/IWFM2001.7"},{"key":"11_CR41","series-title":"International Series in Computer Science","volume-title":"Using Z:\u00a0Specification, Refinement, and Proof","author":"J. Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z:\u00a0Specification, Refinement, and Proof. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1996)"},{"key":"11_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/11921240_2","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"J. Woodcock","year":"2006","unstructured":"Woodcock, J., Freitas, L.: Z\/Eves and the Mondex Electronic Purse. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol.\u00a04281, pp. 15\u201334. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Hybrid Real-Time Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75221-9_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T19:12:10Z","timestamp":1737400330000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75221-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540752202"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75221-9_11","relation":{},"subject":[]}}