{"id":324485,"date":"2016-11-18T19:56:39","date_gmt":"2016-11-19T03:56:39","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-research-item&p=324485"},"modified":"2018-10-16T20:20:33","modified_gmt":"2018-10-17T03:20:33","slug":"theory-program-modifications","status":"publish","type":"msr-research-item","link":"https:\/\/www.microsoft.com\/en-us\/research\/publication\/theory-program-modifications\/","title":{"rendered":"A theory of program modifications"},"content":{"rendered":"
\n

The need to integrate several versions of a program into a common one arises frequently, but it is a tedious and time consuming task to merge programs by hand. The program-integration algorithm proposed by Horwitz, Prins, and Reps provides a way to create a semantics-based<\/em> tool for integrating a base program with two or more variants. The integration algorithm is based on the assumption that any change in the behaviour<\/em>, rather than the text<\/em>, of a program variant is significant and must be preserved in the merged program. An integration system based on this algorithm will determine whether the variants incorporate interfering changes, and, if they do not, create an integrated<\/em> program that includes all changes as well as all features of the base program that are preserved in all variants.<\/p>\n

This paper studies the algebraic properties of the program-integration operation, such as whether there is a law of associativity. (For example, in this context associativity means: \u201cIf three variants of a given base are to be integrated by a pair of two-variant integrations, the same result is produced no matter which two variants are integrated first.\u201d) Whereas an earlier work that studied the algebraic properties of program integration formalized the Horwitz-Prins-Reps integration algorithm as an operation in a Brouwerian algebra<\/em>, this paper introduces a new algebraic structure in which integration can be formalized, called fmalgebra<\/em>. In fm<\/em>-algebra, the notion of integration derives from the concepts of a program modification<\/em> and an operation for combining modifications<\/em>. (Thus, while earlier work concerned an algebra of programs<\/em>, this paper concerns an algebra of program modifications<\/em>.)<\/p>\n

The potential benefits of an algebraic theory of integration, such as the one developed in this paper, are actually three-fold:<\/p>\n

\n
\n
    \n
  1. (1)<\/span>\n
    \n

    It allows one to understand the fundamental algebraic properties of integration\u2014laws that express the \u201cessence of integration.\u201d Such laws allow one to reason formally about the integration operation.<\/p>\n<\/div>\n

    <\/div>\n<\/li>\n
  2. (2)<\/span>\n
    \n

    It provides knowledge that is useful for designing alternative integration algorithms whose power and scope are beyond the capabilities of current algorithms.<\/p>\n<\/div>\n

    <\/div>\n<\/li>\n
  3. (3)<\/span>\n
    \n

    Because such a theory formalizes certain operations that are more primitive than the integration operation, an implementation of these primitive operations can form the basis for a more powerful program-manipulation system than one based on just the integration operation.<\/p>\n<\/div>\n

    <\/div>\n<\/li>\n<\/ol>\n<\/div>\n<\/div>\n<\/section>\n
    \n