{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:33:27Z","timestamp":1694622807838},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2004,4,1]],"date-time":"2004-04-01T00:00:00Z","timestamp":1080777600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2004,4]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>\n            We present a refinement calculus for transforming object-oriented (OO) specifications (or \u2018contracts\u2019) of classes into executable Eiffel programs. The calculus includes the usual collection of algorithmic refinement rules for assignments, if-statements, and loops. However, the calculus also deals with some of the specific challenges of OO, namely rules for introducing\n            <jats:italic>feature calls<\/jats:italic>\n            and reference types (involving aliasing). The refinement process is compositional in the sense that a class specification is refined to code based only on the specifications (not the implementations) of the classes that the specification depends upon. We discuss how automated support for such a process can be developed based on existing tools. This work is done in the context of a larger project involving methods for the seamless design of OO software in the graphical design notation BON (akin to UML). The goal is to maintain model and source code integrity, i.e., the software developer can work on either the model or the code, where (ideally) changes in one view are reflected instantaneously and automatically in all views.\n          <\/jats:p>","DOI":"10.1007\/s00165-003-0024-3","type":"journal-article","created":{"date-parts":[[2004,3,29]],"date-time":"2004-03-29T12:36:13Z","timestamp":1080563773000},"page":"51-79","source":"Crossref","is-referenced-by-count":13,"title":["ERC \u2013 An object-oriented refinement calculus for Eiffel"],"prefix":"10.1145","volume":"16","author":[{"given":"Richard F.","family":"Paige","sequence":"first","affiliation":[{"name":"Department of Computer Science, York University, M3J 1P3, Ontario, Toronto, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonathan S.","family":"Ostroff","sequence":"additional","affiliation":[{"name":"Department of Computer Science, York University, M3J 1P3, Ontario, Toronto, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8598-9","volume-title":"A theory of objects","author":"Abadi M","year":"1996"},{"key":"p_2","volume-title":"The B-book Cambridge","author":"Abr J-R","year":"1996"},{"key":"p_3","volume-title":"Proceedings of formal methods pacific (FMP'97)","author":"Bancroft PG","year":"1997"},{"key":"p_4","volume-title":"Proceedings of TACAS 2001. LNCS 2031. Springer, Berlin Heidelberg New York","author":"van den Berg J","year":"2001"},{"key":"p_5","doi-asserted-by":"crossref","DOI":"10.1109\/32.879810","article-title":"A weakest-precondition semantics for refinement object-oriented programs","author":"Cavalcanti A","year":"2000","journal-title":"IEEE Trans Software Eng 26(8)"},{"key":"p_6","volume-title":"An inconsistency in procedures, parameters, and substitution in the refinement calculus. Sci Comput Programming 33(87-96)","author":"Cavalcanti A","year":"1999"},{"key":"p_7","volume-title":"Proceedings of WIFT'95","author":"Crow J","year":"1995"},{"key":"p_10","volume-title":"Getting started with perfect. Available from www.eschertech.com","author":"Esc","year":"2000"},{"key":"p_11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3837-7","volume-title":"A logical approach to discrete mathematics","author":"Gries D","year":"1993"},{"key":"p_13","volume-title":"A practical theory of programming","author":"Heh ECR","year":"1993"},{"key":"p_14","volume-title":"Communicating sequential processes","author":"Hoa CAR","year":"1985"},{"key":"p_15","volume-title":"Design-by-Contract: the lessons of the Ariane 5","author":"Jezequel J-M","year":"1997"},{"key":"p_16","volume-title":"Systematic software development using VDM","author":"Jon CB","year":"1990","edition":"2"},{"key":"p_17","volume-title":"Quantified assertions in Eiffel","author":"Kent S","year":"1995"},{"key":"p_18","volume-title":"Formal object-oriented development","author":"Lan K","year":"1995"},{"key":"p_19","volume-title":"Larch\/C++ Reference Manual Version 5.14.","author":"Lea G","year":"1997"},{"key":"p_22","volume-title":"Proceedings of the fourth international workshop on foundations of object-oriented languages","author":"Lei KRM","year":"1997"},{"issue":"1","key":"p_23","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1016\/S0304-3975(98)00165-0","article-title":"Joining specification statements","volume":"216","author":"Leino KRM","year":"1999","journal-title":"Theor Comput Sci"},{"key":"p_24","volume-title":"ESC\/Java user's manual. Technical Note 2000-002","author":"Leino KRM","year":"2000"},{"key":"p_25","volume-title":"A behavioural notion of subtyping. ACM Trans Programming Language Syst 16(6)","author":"Liskov B","year":"1994"},{"key":"p_26","volume-title":"Eiffel: the language","author":"Mey B","year":"1992"},{"key":"p_27","volume-title":"Object-oriented software construction","author":"Mey B","year":"1997","edition":"2"},{"key":"p_28","volume-title":"Agents, iterators, introspection","author":"Mey B","year":"2000"},{"key":"p_29","volume-title":"Proceedings of ZB-2003","author":"Mey B","year":"2003"},{"key":"p_30","volume-title":"Programming from specifications","author":"Mor CC","year":"1994","edition":"2"},{"key":"p_32","volume-title":"Proceedings the of world congress on formal methods (FM'99). Vol I. LNCS 1708","author":"Paige RF","year":"1999"},{"key":"p_33","volume-title":"Proceedings of the fundamental aspects of software engineering (FASE'01). LNCS","author":"Paige RF","year":"2001"},{"key":"p_35","volume-title":"A technique for software module specification with examples. Commun ACM 15(5)","author":"Par DL","year":"1972"},{"key":"p_36","volume-title":"On the criteria to be used in decomposing systems into modules. Commun ACM 15(12)","author":"Par D","year":"1972"},{"key":"p_38","volume-title":"Proceedings of unified modeling language 2000. LNCS 1939. Springer, Berlin Heidelberg New York","author":"Richters M","year":"2000"},{"key":"p_39","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511663079","volume-title":"Data refinement: model-oriented proof methods and their comparison","author":"de Roever W-P","year":"1998"},{"key":"p_40","volume-title":"The unified modeling language reference manual","author":"Rumbaugh J","year":"1999"},{"key":"p_41","volume-title":"Proceedings of the asia-pacific software engineering conference","author":"Smi G","year":"1995"},{"key":"p_42","volume-title":"The object-Z specification language","author":"Smi G","year":"2000"},{"key":"p_43","volume-title":"Proceedings of the international conference on formal engineering methods","author":"Smi G","year":"2002"},{"key":"p_44","volume-title":"The Z reference manual","author":"Spi JM","year":"1992","edition":"2"},{"key":"p_45","volume-title":"Seamless object-oriented software architecture","author":"Walden K","year":"1995"},{"key":"p_46","volume-title":"Software development with Z","author":"Wor J","year":"1994"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-003-0024-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-003-0024-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-003-0024-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:35:30Z","timestamp":1641483330000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-003-0024-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,4]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2004,4]]}},"alternative-id":["10.1007\/s00165-003-0024-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-003-0024-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,4]]}}}