{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:49:54Z","timestamp":1750308594532,"version":"3.41.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2017,1,5]],"date-time":"2017-01-05T00:00:00Z","timestamp":1483574400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2017,1,5]]},"abstract":"<jats:p>Writing specifications about program behavior is hard. Writing specifications about non-functional effects such as resource usage is often even harder. If manually instrumenting the program is not an option, programmers have to rely on comment-based specification languages like JML to introduce ghost variables and other fairly abstract concepts that are complicated and hard to maintain. Even worse, most static analysis tools nowadays operate on bit- or bytecode and cannot process those type of specifications<\/jats:p>\n          <jats:p>To address this problem, we propose a library-based specification formalism for time complexity in Java. The approach is inspired by the success of assertion libraries like CodeContracts and Guava. Our library provides a set of methods and enumerated types that allow the user to write complexity assertions in a 'human' readable form and without instrumenting the code. On the backend, we provide a bytecode rewriting tool that uses these assertions to automatically instrument the program with counter variables. The transformed program can then be checked via testing or off-the-shelf automated static analyzers<\/jats:p>","DOI":"10.1145\/3011286.3011294","type":"journal-article","created":{"date-parts":[[2017,1,6]],"date-time":"2017-01-06T13:30:07Z","timestamp":1483709407000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Resource Contracts for Java"],"prefix":"10.1145","volume":"41","author":[{"given":"Rody","family":"Kersten","sequence":"first","affiliation":[{"name":"CMU Silicon Valley"}]},{"given":"Martin","family":"Sch\u00e4f","sequence":"additional","affiliation":[{"name":"SRI International"}]},{"given":"Temesghen","family":"Kahsai","sequence":"additional","affiliation":[{"name":"CMU Silicon Valley \/ NASA Ames"}]}],"member":"320","published-online":{"date-parts":[[2017,1,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929501.1929513"},{"volume-title":"Praxis Critical Systems Limited","year":"2006","author":"Barnes J.","key":"e_1_2_1_2_1"},{"key":"e_1_2_1_3_1","unstructured":"P. Baudin P. Cuoq J.-C. Filli\u00e2tre C. March\u00e9 B. Monate Y. Moy and V. Prevosto. ACSL: ANSI\/ISO C Specification Language ver. 1.5 2010.  P. Baudin P. Cuoq J.-C. Filli\u00e2tre C. March\u00e9 B. Monate Y. Moy and V. Prevosto. ACSL: ANSI\/ISO C Specification Language ver. 1.5 2010."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_6"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"volume-title":"Prentice-Hall","year":"1976","author":"Dijkstra E. W.","key":"e_1_2_1_7_1"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18070-5_2"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_35"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_7"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"J. J\u00e9z\u00e9quel and B. Meyer. Design by contract: The lessons of Ariane. IEEE Computer 30(1) 1997.  J. J\u00e9z\u00e9quel and B. Meyer. Design by contract: The lessons of Ariane. IEEE Computer 30(1) 1997.","DOI":"10.1109\/2.562936"},{"volume-title":"Oxford University","year":"1981","author":"Jones C.","key":"e_1_2_1_13_1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_19"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12466-7_6"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.3154"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2388936.2388959"},{"volume-title":"Formal Underpinnings of Java Workshop (at OOPSLA '98)","year":"1998","author":"Leavens G. T.","key":"e_1_2_1_18_1"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297846.1297902"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390635"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958101"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1852761.1852776"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2012.19"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_4"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347389"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3011286.3011294","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3011286.3011294","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:28Z","timestamp":1750273528000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3011286.3011294"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,5]]},"references-count":29,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2017,1,5]]}},"alternative-id":["10.1145\/3011286.3011294"],"URL":"https:\/\/doi.org\/10.1145\/3011286.3011294","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2017,1,5]]},"assertion":[{"value":"2017-01-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}