A rule-based language for programming software updates

ABSTRACT

We describe the design of a rule-based language for expressing changes to Haskell programs in a systematic and reliable way. The update language essentially offers update commands for all constructs of the object language (a subset of Haskell). The update language can be translated into a core calculus consisting of a small set of basic updates and update combinators. The key construct of the core calculus is a scope update mechanism that allows (and enforces) update specifications for the definition of a symbol together with all of its uses.The type of an update program is given by the possible type changes it can cause for an object programs. We have developed a type-change inference system to automatically infer type changes for updates. Updates for which a type change can be successfully inferred and that satisfy an additional structural condition can be shown to preserve type correctness of object programs.In this paper we define the Haskell Update Language HULA and give a translation into the core update calculus. We illustrate HULA and its translation into the core calculus by several examples.

REFERENCES

• 1: ACM. Communications of the ACM, volume 44(10), October 2001.
• 2: N. Bjørner. Type Checking Meta Programs. In Workshop on Logical Frameworks and Meta-Languages, 1999.
• 3: B. Borovanský, C. Kirchner, H. Kirchner, P. E. Moreau, and C. Ringeissen. Rewriting with Strategies in ELAN: a Functional Semantics. Int. Journal of Foundations of Computer Science, 2001. To appear.
• 4: B. Borovanský, C. Kirchner, H. Kirchner, P. E. Moreau, and M. Vittek. ELAN: A Logical Framework Based on Computational Systems. In Workshop on Rewriting Logic and Applications, 1996.
• 5: P. Borras , D. Clement , Th. Despeyroux , J. Incerpi , G. Kahn , B. Lang , V. Pascual, Centaur: the system, Proceedings of the third ACM SIGSOFT/SIGPLAN software engineering symposium on Practical software development environments, p.14-24, November 28-30, 1988, Boston, Massachusetts, United States
• 6: James R. Cordy , Charles D. Halpern-Hamu , Eric Promislow, TXL: a rapid prototyping system for programming language dialects, Computer Languages, v.16 n.1, p.97-107, 1991 [doi>10.1016/0096-0551(91)90019-6]
• 7: Martin Erwig, Programs Are Abstract Data Types, Proceedings of the 16th IEEE international conference on Automated software engineering, p.400, November 26-29, 2001
• 8: M. Erwig. Update your Program? Program Your Update! Technical Report TR02-60-01, Department of Computer Science, Oregon State University, 2002. http://www.cs.orst.edu/~erwig/papers/up.pdf.
• 9: M. Erwig and D. Ren. An Update Calculus for Type-Safe Program Changes. 2002. submitted for publication. http://www.cs.orst.edu/~erwig/papers/uc.pdf.
• 10: Refactoring: improving the design of existing code, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 11: Gregor Kiczales , Erik Hilsdale , Jim Hugunin , Mik Kersten , Jeffrey Palm , William Griswold, Getting started with ASPECTJ, Communications of the ACM, v.44 n.10, p.59-65, Oct. 2001 [doi>10.1145/383845.383858]
• 12: Ralf Lämmel , Joost Visser, Typed Combinators for Generic Traversal, Proceedings of the 4th International Symposium on Practical Aspects of Declarative Languages, p.137-154, January 19-20, 2002
• 13: Dale Miller, Abstract Syntax for Variable Binders: An Overview, Proceedings of the First International Conference on Computational Logic, p.239-253, July 01, 2000
• 14: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 15: S. L. Peyton Jones, J. Hughes, et al. Report on the Programming Language Haskell 98, 1999. http://haskell.org/onlinereport.
• 16: Frank Pfenning, Logical frameworks, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
• 17: F. Pfenning , C. Elliot, Higher-order abstract syntax, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.199-208, June 20-24, 1988, Atlanta, Georgia, United States
• 18: Thomas W. Reps , Tim Teitelbaum, The synthesizer generator: a system for constructing language-based editors, Springer-Verlag New York, Inc., New York, NY, 1989
• 19: D. Roberts and J. Brant. Refactoring Tools. In M. Fowler, editor, Refactoring: Improving the Design of Existing Code, chapter 14, pages 309-352. Addison-Wesley, Reading, MA, 1999.
• 20: Tim Sheard, Accomplishments and Research Challenges in Meta-programming, Proceedings of the Second International Workshop on Semantics, Applications, and Implementation of Program Generation, p.2-44, September 06, 2001
• 21: Walid Taha , Tim Sheard, MetaML and multi-stage programming with explicit annotations, Theoretical Computer Science, v.248 n.1-2, p.211-242, October 2000 [doi>10.1016/S0304-3975(00)00053-0 ]
• 22: C. Verhoef, Towards automated modification of legacy assets, Annals of Software Engineering, v.9 n.1-4, p.315-336, 2000
• 23: Eelco Visser, Strategic Pattern Matching, Proceedings of the 10th International Conference on Rewriting Techniques and Applications, p.30-44, July 02-04, 1999
• 24: E. Visser. Language Independent Traversals for Program Transformation. In Workshop on Generic Programming, 2000. Technical Report UU-CS-2000-19, Universiteit Utrecht.
• 25: Eelco Visser, Stratego: A Language for Program Transformation Based on Rewriting Strategies, Proceedings of the 12th International Conference on Rewriting Techniques and Applications, p.357-362, May 22-24, 2001
• 26: Eelco Visser , Zine-el-Abidine Benaissa , Andrew Tolmach, Building program optimizers with rewriting strategies, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.13-26, September 26-29, 1998, Baltimore, Maryland, United States
• 27: E. Visser, et al. The Online Survey of Program Transformation. http://www.program-transformation.org/survey.html.
• 28: Jon Whittle , Alan Bundy , Helen Lowe, An Editor for Helping Novices to Learn Standard ML, Proceedings of the9th International Symposium on Programming Languages: Implementations, Logics, and Programs: Including a Special Trach on Declarative Programming Languages in Education, p.389-405, September 03-05, 1997

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.2 Automatic Programming
  D.2 SOFTWARE ENGINEERING
      D.2.7 Distribution, Maintenance, and Enhancement

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Design, Languages, Reliability

Keywords:
type change, type correctness, update program, update safey