{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,23]],"date-time":"2024-12-23T23:40:06Z","timestamp":1734997206472,"version":"3.32.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[1997,5,1]],"date-time":"1997-05-01T00:00:00Z","timestamp":862444800000},"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":[[1997,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Imperative programs can be inverted directly from their forward-directed program code with the use of logical inference. The relational semantics of imperative computations treats programs as logical relations over the observable state of the environment, which is taken to be the state of the variables in memory. Program relations denote both forward and backward computations, and the direction of the computation depends upon the instantiation pattern of arguments in the relation. This view of inversion has practical applications when the relational semantics is treated as a logic program. Depending on the logic programming inference scheme used, execution of this relational program can compute the inverse of the imperative program. A number of nontrivial imperative computations can be inverted with minimal logic programming tools.<\/jats:p>","DOI":"10.1007\/bf01211087","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T15:42:36Z","timestamp":1109346156000},"page":"331-348","source":"Crossref","is-referenced-by-count":22,"title":["Running programs backwards: The logical inversion of imperative computation"],"prefix":"10.1145","volume":"9","author":[{"given":"Brian J.","family":"Ross","sequence":"first","affiliation":[{"name":"Department of Computer Science, Brock University, L2S 3A1, St Catharines, Ontario, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1147\/rd.176.0525"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02084158"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037639"},{"issue":"3","key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1145\/357103.357108","article-title":"Derivation of invariant assertions during program development by transformation","volume":"2","author":"Broy M.","year":"1980","journal-title":"TOPLAS"},{"key":"e_1_2_1_2_5_2","unstructured":"Clark K.L. Predicate Logic as a Computational Formalism. Technical Report 79\/59 Imperial College December 1979."},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Clocksin W.F. and Mellish C.S. Programming in Prolog (3rd ed) . Springer-Verlag 1987.","DOI":"10.1007\/978-3-642-97005-4"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90042-C"},{"issue":"1","key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/TSE.1981.234508","article-title":"Consequence verification of flowcharts","volume":"7","author":"Clark K.L.","year":"1981","journal-title":"IEEE Transactions on Software Engineering"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(81)90014-X"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Dijkstra E.W. EWD671: Program inversion. In Selected Writings on Computing: A Personal Perspective pages 351\u2013354. Springer-Verlag 1982.","DOI":"10.1007\/978-1-4612-5695-3_63"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Gries D. The Science of Programming . Springer-Verlag 1981.","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"e_1_2_1_2_12_2","unstructured":"Gries D. and van de Snepscheut J.L.A. Inorder traversal of a binary tree and its inversion. In E.W. Dijkstra editor Formal Development of Programs and Proofs pages 37\u201342. Addison Wesley 1990."},{"key":"e_1_2_1_2_13_2","unstructured":"Harrison P.G. and Khoshnevisan H. On the Synthesis of Function Inverses. Technical report Imperial College 1986."},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3729.001.0001","volume-title":"Induction","author":"Holland J.H.","year":"1986"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Hoare C. A. R. Communicating Sequential Processes . Prentice-Hall 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Hogger C. J. Essentials of Logic Programming . Oxford University Press 1990.","DOI":"10.1093\/oso\/9780198538202.001.0001"},{"key":"e_1_2_1_2_17_2","unstructured":"Hopcroft J.E. and Ullman J.D. Introduction to Automata Theory Languages and Computation . Addison Wesley 1979."},{"key":"e_1_2_1_2_18_2","unstructured":"Knuth Donald E. Seminumerical Algorithms . Addison-Wesley 2nd edition 1981."},{"key":"e_1_2_1_2_19_2","unstructured":"Korf R.E. Inversion of applicative programs. In IJCAI pages 1007\u20131009 1981."},{"issue":"1","key":"e_1_2_1_2_20_2","first-page":"50","article-title":"A formal approach to undo operations in programming languages","volume":"8","author":"Leeman G.B.","year":"1986","journal-title":"Journal of the ACM"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Lloyd J.W. Foundations of Logic Programming (2nd ed) . Springer-Verlag 1987.","DOI":"10.1007\/978-3-642-83189-8"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"McCarthy J. The inversion of functions defined by turing machines. In C.E. Shannon and J. McCarthy editors Automata Studies pages 177\u2013181. Princeton University Press 1956.","DOI":"10.1515\/9781400882618-009"},{"key":"e_1_2_1_2_23_2","unstructured":"Ross B.J. The partial evaluation of imperative programs using prolog. In Metaprogramming in Logic Programming pages 341\u2013363. MIT Press 1989."},{"key":"e_1_2_1_2_24_2","unstructured":"Sperschneider V. and Antoniou G. Logic: A Foundation for Computer Science . Addison Wesley 1991."},{"key":"e_1_2_1_2_25_2","unstructured":"Sickel S. Invertibility of logic programs. In 4th Workshop on Automated Deduction pages 103\u2013109 Austin Texas February 1\u20133 1979."},{"key":"e_1_2_1_2_26_2","unstructured":"Shoham Y. and McDermott D.V. Directed relations and inversion of prolog programs. In International Conference on Fifth Generation Computer Systems pages 307\u2013316 1984."},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(85)90019-6"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Toffoli T. and Margolus N. Invertible cellular automata: a review. Physica D Nonlinear Phenomena 45(1\u20133) 1990.","DOI":"10.1016\/0167-2789(90)90185-R"},{"volume-title":"What Computing is All About","year":"1993","author":"van de Snepscheut J.L.A.","key":"e_1_2_1_2_29_2"},{"key":"e_1_2_1_2_30_2","unstructured":"van Hentenryck P. Constraint Satisfaction in Logic Programming . MIT Press 1990."},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90141-4"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211087.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211087\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211087","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,23]],"date-time":"2024-12-23T23:05:43Z","timestamp":1734995143000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211087"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,5]]},"references-count":31,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1997,5]]}},"alternative-id":["10.1007\/BF01211087"],"URL":"https:\/\/doi.org\/10.1007\/bf01211087","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[1997,5]]}}}