{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,15]],"date-time":"2023-05-15T17:40:09Z","timestamp":1684172409285},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2009,8,1]],"date-time":"2009-08-01T00:00:00Z","timestamp":1249084800000},"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":[[2009,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The SCOOP model extends the Eiffel programming language to provide support for concurrent programming. The model is based on the principles of Design by Contract. The semantics of contracts used in the original proposal (SCOOP_97) is not suitable for concurrent programming because it restricts parallelism and complicates reasoning about program correctness. This article outlines a new contract semantics which applies equally well in concurrent and sequential contexts and permits a flexible use of contracts for specifying the mutual rights and obligations of clients and suppliers while preserving the potential for parallelism. We argue that it is indeed a generalisation of the traditional correctness semantics. We also propose a proof technique for concurrent programs which supports proofs\u2014similar to those for traditional non-concurrent programs\u2014of partial correctness and loop termination in the presence of asynchrony.<\/jats:p>","DOI":"10.1007\/s00165-007-0063-2","type":"journal-article","created":{"date-parts":[[2008,1,3]],"date-time":"2008-01-03T12:58:23Z","timestamp":1199365103000},"page":"305-318","source":"Crossref","is-referenced-by-count":8,"title":["Contracts for concurrency"],"prefix":"10.1145","volume":"21","author":[{"given":"Piotr","family":"Nienaltowski","sequence":"first","affiliation":[{"name":"Praxis High Integrity Systems Limited, 20 Manvers Street, BA1 1PX, Bath, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bertrand","family":"Meyer","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonathan S.","family":"Ostroff","sequence":"additional","affiliation":[{"name":"York University, Toronto, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Adrian C (2002) SCOOP for SmallEiffel. draft available online at http:\/\/www.chez.com\/cadrian\/eiffel\/scoop.html June 2002"},{"key":"e_1_2_1_2_2_2","volume-title":"Dependable systems: software, computing, networks","author":"Arslan V","year":"2006"},{"key":"e_1_2_1_2_3_2","unstructured":"Arslan V Meyer B (2006) Asynchronous exceptions in concurrent object-oriented programming. In: International Symposium on Concurrency Real-Time and Distribution in Eiffel-like Languages (CORDIE) York UK July 2006"},{"key":"e_1_2_1_2_4_2","unstructured":"Bailly A (2004) Formal semantics and proof system for SCOOP. White paper October 2004"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Barnett M Leino KRM Schulte W (2004) The Spec programming system: an overview. In: CASSIS vol 3362 of LNCS. Springer Heidelberg","DOI":"10.1007\/978-3-540-30569-9_3"},{"issue":"10","key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","first-page":"111","DOI":"10.5381\/jot.2007.6.10.a4","article-title":"Exceptions in Concurrent Eiffel","volume":"6","author":"Brooke PJ","year":"2007","journal-title":"J Object Technol"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/162685.162711"},{"key":"e_1_2_1_2_8_2","unstructured":"Gunaseelan L LeBlanc RJ (1992) Distributed eiffel: a language for programming multigranular objects. In: 4th International conference on computer languages San Francisco"},{"key":"e_1_2_1_2_9_2","unstructured":"Jalloul G (1994) Concurrent object-oriented systems: a disciplined approach. PhD thesis University of Technology Sydney"},{"key":"e_1_2_1_2_10_2","unstructured":"Jones CB (1981) Development methods for computer programs including a notion of interference. PhD thesis Oxford University"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Jones CB (2003) Wanted: a compositional approach to concurrency Chapter 1. Springer Heidelberg pp 1\u201315","DOI":"10.1007\/978-0-387-21798-7_1"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/141937.141964"},{"key":"e_1_2_1_2_13_2","unstructured":"Leavens GT Poll E Clifton C Cheon Y Ruby v Cok DR Kiniry J (2005) JML reference manual. Iowa State University Department of Computer Science"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1981.230844"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/261119"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.5555\/211468"},{"key":"e_1_2_1_2_18_2","unstructured":"Nienaltowski P (2007) Flexible access control policy for SCOOP. Formal Aspects of Computing special issue: Concurrency Real-Time and Distribution in Eiffel-like Languages (CORDIE) (to appear)"},{"key":"e_1_2_1_2_19_2","unstructured":"Nienaltowski P (2007) Practical framework for contract-based concurrent object-oriented programming. PhD thesis no. 17061 Department of Computer Science ETH Zurich"},{"key":"e_1_2_1_2_20_2","unstructured":"Ostroff J Torshizi FA Huang HF Schoeller B (2007) Beyond contracts for concurrency. Formal Aspects of Computing special issue: Concurrency Real-Time and Distribution in Eiffel-like Languages (CORDIE) (to appear)"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Rodriguez E Dwyer M Flanagan C Hatcliff J Leavens GT Robby (2005) Extending JML for modular specification and verification of multi-threaded programs. In: European Conference on Object-Oriented Programming (ECOOP) pp 551\u2013576","DOI":"10.1007\/11531142_24"},{"key":"e_1_2_1_2_22_2","unstructured":"Sutton SM (1995) Preconditions postconditions and provisional execution in software processes. Technical Report UM-CS-1995-077 University of Massachusetts Amherst"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-007-0063-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-007-0063-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-007-0063-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,15]],"date-time":"2023-05-15T17:11:13Z","timestamp":1684170673000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-007-0063-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,8]]},"references-count":22,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,8]]}},"alternative-id":["10.1007\/s00165-007-0063-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-007-0063-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,8]]}}}