{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T23:16:51Z","timestamp":1649027811090},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2017,5,1]],"date-time":"2017-05-01T00:00:00Z","timestamp":1493596800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100012913","name":"Tata Consultancy Services","doi-asserted-by":"crossref","award":["12TCSRSP001"],"award-info":[{"award-number":["12TCSRSP001"]}],"id":[{"id":"10.13039\/100012913","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>In the correct-by-construction programming methodology, programs are incrementally derived from their formal specifications, by repeatedly applying transformations to partially derived programs. At an intermediate stage in a derivation, users may have to make certain assumptions to proceed further. To ensure that the assumptions hold true at that point in the program, certain other assumptions may need to be introduced upstream as loop invariants or preconditions. Typically these other assumptions are made in an ad hoc fashion and may result in unnecessary rework, or worse, complete exclusion of some of the alternative solutions. In this work, we present rules for propagating assumptions through annotated programs. We show how these rules can be integrated in a top-down derivation methodology to provide a systematic approach for propagating the assumptions, materializing them with executable statements at a place different from the place of introduction, and strengthening of loop invariants with minimal additional proof efforts.<\/jats:p>","DOI":"10.1007\/s00165-016-0395-x","type":"journal-article","created":{"date-parts":[[2016,10,26]],"date-time":"2016-10-26T07:06:33Z","timestamp":1477465593000},"page":"495-530","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Assumption propagation through annotated programs"],"prefix":"10.1145","volume":"29","author":[{"given":"Dipak L.","family":"Chaudhari","sequence":"first","affiliation":[{"name":"Indian Institute of Technology Bombay, Mumbai, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Om","family":"Damani","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Bombay, Mumbai, India"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Butler M L\u00e5ngbacka T (1996) Program derivation using the refinement calculator. In: Theorem proving in higher order logics: 9th international conference LNCS vol 1125. Springer Verlag Berlin pp 93\u2013108","DOI":"10.1007\/BFb0105399"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Backhouse R Michaelis D (2006) Exercises in quantifier manipulation. In: Mathematics of program construction. Springer Berlin pp 69\u201381","DOI":"10.1007\/11783596_7"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Barrett C Tinelli C (2007) CVC3. In: Damm W Hermanns H (eds) CAV LNCS vol 4590. Springer Berlin pp 298\u2013302","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Back R-J von Wright J (1998) Refinement calculus: a systematic introduction. Graduate texts in computer science. Springer New York","DOI":"10.1007\/978-1-4612-1674-2_1"},{"key":"e_1_2_1_2_5_2","unstructured":"Bobot F Conchon S Contejean E Iguernelala M Lescuyer S Mebsout A (2008) The alt-ergo automated theorem prover"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Chaudhari DL Damani O (2014) Automated theorem prover assisted program calculations. In: Albert E Sekerinski E (eds)\nIntegrated formal methods Lecture Notes in Computer Science. Springer Switzerland pp 205\u2013220","DOI":"10.1007\/978-3-319-10181-1_13"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Chaudhari DL Damani OP (2015) Combining top-down and bottom-up techniques in program derivation. In: Logic-Based program synthesis and transformation\u201425th international symposium LOPSTR 2015 Siena Italy July 13\u201315 2015. Revised Selected Papers pp 244\u2013258","DOI":"10.1007\/978-3-319-27436-2_15"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Carrington D Hayes I Nickson R Watson GN Welsh J (1996) A tool for developing correct programs by refinement. Technical report","DOI":"10.14236\/ewic\/RW1996.3"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.5555\/91408"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_2_11_2","volume-title":"A discipline of programming","author":"Dijkstra EW","year":"1976"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"De Moura L Bj\u00f8rner N (2008) Z3: an efficient smt solver. In: Tools and algorithms for the construction and analysis of systems. Springer Berlin","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/77545"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre J-C Paskevich A (2013) Why3\u2014where programs meet provers. In: ESOP\u201913 22nd European Symposium on Programming LNCS vol 7792 Rome. Springer Berlin","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_1_2_15_2","unstructured":"Michael Franssen Cocktail.: A tool for deriving correct programs. In Workshop on Automated Reasoning 1999."},{"key":"e_1_2_1_2_16_2","unstructured":"Gries D (1987) The science of programming 1st edn. Springer New York Inc. Secaucus"},{"key":"e_1_2_1_2_17_2","unstructured":"Groves L (1998) Adapting program derivations using program conjunction. In: International Refinement Workshop And Formal Methods Pacific vol 98. Citeseer pp 145\u2013164"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. CACM Commun ACM p 12","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.5555\/98158"},{"key":"e_1_2_1_2_20_2","unstructured":"Laibinis L von Wright J (1997) Context handling in the refinement calculus framework. Technical Report TUCS-TR-118 Turku Centre for Computer Science Finland August 21"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.5555\/95423"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Oliveira M Xavier M Cavalcanti A (2004) Refine and gabriel: support for refinement and tactics. In: Software engineering and formal methods 2004. SEFM 2004. Proceedings of the Second International Conference on. IEEE pp 310\u2013319","DOI":"10.1109\/SEFM.2004.1347535"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Weidenbach C Brahm U Hillenbrand T Keen E Theobalt C Topic D (2002) SPASS version 2.0. In: Voronkov A (ed) Automated deduction\u2014CADE-18 Lecture notes in computer science vol 2392. Springer Berlin pp 275\u2013279","DOI":"10.1007\/3-540-45620-1_22"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0395-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0395-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0395-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0395-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:55:54Z","timestamp":1641538554000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0395-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5]]},"references-count":23,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,5]]}},"alternative-id":["10.1007\/s00165-016-0395-x"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0395-x","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,5]]}}}