{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/21206"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/21206","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"The replay of program derivations","abstract":"A promising though radical approach to software development is to write formal specifications and then derive implementations by applying sequences of formal steps. This is often known as transformational implementation. An advantage of this approach is increased consistency between specifications and implementations. But perhaps a more important advantage is the potential for maintaining specifications rather than implementations. Because derivation sequences formally describe how implementations are constructed, the user can modify specifications and then replay the derivations to obtain new implementations.","abstract_html":"A promising though radical approach to software development is to write formal specifications and then derive implementations by applying sequences of formal steps. This is often known as transformational implementation. An advantage of this approach is increased consistency between specifications and implementations. But perhaps a more important advantage is the potential for maintaining specifications rather than implementations. Because derivation sequences formally describe how implementations are constructed, the user can modify specifications and then replay the derivations to obtain new implementations.","abstract_has_math":false,"creators":["Hasker, Robert W."],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Reddy, Uday S."],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2011,"date_issued":"2011-05-07T13:01:38Z","date_published":"2011-05-07T13:01:38Z","updated_at":"2026-07-22T22:25:17Z","subjects":["Computer Science"],"languages":["eng"],"rights":["Copyright 1995 Hasker, Robert W."],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["AAI9522116","(UMI)AAI9522116"],"render_values":[{"text":"AAI9522116","href":null,"code":true},{"text":"(UMI)AAI9522116","href":null,"code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/2142/21206","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Reddy, Uday S."]},{"key":"dc:creator","label":"Author","values":["Hasker, Robert W."]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2011-05-07T13:01:38Z","10000-01-01","1995"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Computer Science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 1995 Hasker, Robert W."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["AAI9522116","(UMI)AAI9522116","http://hdl.handle.net/2142/21206"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["A promising though radical approach to software development is to write formal specifications and then derive implementations by applying sequences of formal steps. This is often known as transformational implementation. An advantage of this approach is increased consistency between specifications and implementations. But perhaps a more important advantage is the potential for maintaining specifications rather than implementations. Because derivation sequences formally describe how implementations are constructed, the user can modify specifications and then replay the derivations to obtain new implementations.","This thesis discusses replaying derivations in an interactive environment. We identify several problems which need to be addressed to make replay both autonomous and robust. We present our implemented replay system, ReFocus, and describe how it addresses these problems. In particular, we present methods for updating derivations to match new specifications and for verifying the acceptability of implementations produced by replay.","Updating derivations represents the technical core of this thesis. The system constructs analogical maps between specifications and applies them to derivations to solve new problems. Traditionally, analogical maps are constructed using first-order generalization, or anti-unification. However, we show that first-order generalization is too inflexible for program derivations. In its place, we propose using second-order generalization. We give a definition of second-order generalization, identify classes of terms for which such generalizations exist, and show that it is computable. We then identify an important subset of generalizations and give (under assumptions) a quadratic-time algorithm for computing this subset. Finally, we show that these generalizations provide the necessary flexibility for replay.","We give a number of examples illustrating the usefulness of replay on small to medium-sized problems. For each, we show that ReFocus is able to obtain useful results. This demonstrates that replaying program derivations is both feasible and useful.","Made available in DSpace on 2011-05-07T13:01:38Z (GMT). No. of bitstreams: 2 license.txt: 4922 bytes, checksum: 910b249b4beec47e7ab768910c8f966f (MD5) 9522116.pdf: 8485085 bytes, checksum: db1a78d9277c3fc2279ac17f2efee7df (MD5) Previous issue date: 1995","Item marked as restricted to the 'UIUC Users [automated]' Group (id=2) by Howard Ding (hding2@illinois.edu) on 2011-05-07T14:49:12Z Item is restricted indefinitely.","Restriction data tranferred 2014-07-01T11:22:21-05:00 Original Data Group with Access UIUC Users [automated] Release Date: none Reason: ETDs are only available to UIUC Users without author permission","ETDs are only available to UIUC Users without author permission","U of I Only"]},{"key":"dc:title","label":"Title","values":["The replay of program derivations"]}]}],"canonical_facts":{"dc:contributor":["Reddy, Uday S."],"dc:creator":["Hasker, Robert W."],"dc:date":["2011-05-07T13:01:38Z","10000-01-01","1995"],"dc:description":["A promising though radical approach to software development is to write formal specifications and then derive implementations by applying sequences of formal steps. This is often known as transformational implementation. An advantage of this approach is increased consistency between specifications and implementations. But perhaps a more important advantage is the potential for maintaining specifications rather than implementations. Because derivation sequences formally describe how implementations are constructed, the user can modify specifications and then replay the derivations to obtain new implementations.","This thesis discusses replaying derivations in an interactive environment. We identify several problems which need to be addressed to make replay both autonomous and robust. We present our implemented replay system, ReFocus, and describe how it addresses these problems. In particular, we present methods for updating derivations to match new specifications and for verifying the acceptability of implementations produced by replay.","Updating derivations represents the technical core of this thesis. The system constructs analogical maps between specifications and applies them to derivations to solve new problems. Traditionally, analogical maps are constructed using first-order generalization, or anti-unification. However, we show that first-order generalization is too inflexible for program derivations. In its place, we propose using second-order generalization. We give a definition of second-order generalization, identify classes of terms for which such generalizations exist, and show that it is computable. We then identify an important subset of generalizations and give (under assumptions) a quadratic-time algorithm for computing this subset. Finally, we show that these generalizations provide the necessary flexibility for replay.","We give a number of examples illustrating the usefulness of replay on small to medium-sized problems. For each, we show that ReFocus is able to obtain useful results. This demonstrates that replaying program derivations is both feasible and useful.","Made available in DSpace on 2011-05-07T13:01:38Z (GMT). No. of bitstreams: 2 license.txt: 4922 bytes, checksum: 910b249b4beec47e7ab768910c8f966f (MD5) 9522116.pdf: 8485085 bytes, checksum: db1a78d9277c3fc2279ac17f2efee7df (MD5) Previous issue date: 1995","Item marked as restricted to the 'UIUC Users [automated]' Group (id=2) by Howard Ding (hding2@illinois.edu) on 2011-05-07T14:49:12Z Item is restricted indefinitely.","Restriction data tranferred 2014-07-01T11:22:21-05:00 Original Data Group with Access UIUC Users [automated] Release Date: none Reason: ETDs are only available to UIUC Users without author permission","ETDs are only available to UIUC Users without author permission","U of I Only"],"dc:identifier":["AAI9522116","(UMI)AAI9522116","http://hdl.handle.net/2142/21206"],"dc:language":["eng"],"dc:rights":["Copyright 1995 Hasker, Robert W."],"dc:subject":["Computer Science"],"dc:title":["The replay of program derivations"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:17Z"}