Topic: transformation of programs

topics > computer science > programming > Group: program proving

abstraction in programming
code optimization by global analysis
constructing proof and program together
executable code from specifications and designs
incremental development
object slice
object transformation language
no need for efficiency
programming as mathematics
stepwise refinement
string transformation languages
structure transformation languages


Program transforms allow writing programs in a very high-level description. The high-level description makes these programs portable, easy to write, easy to modify, and provably correct. Program transforms makes the description efficient. They are high level optimization techniques which transform programs into equivalent representations. Many techniques of global optimization may fall into this category. For instance common sub-expression elimination or code movement outside of loops. Other transforms convert recursive functions into non-recursive repetitions, e.g., tail recursion is transformed to a simple loop. Reduction languages are based on program transforms of expressions; besides using program transforms to find efficient equivalents to expression representations.

Program transforms are not widely used because the determination of transforms is difficult, and the known set of transforms is insufficient for real programs. These difficulties would be insurmountable if global rearrangement is fundamentally a human process. (cbb 5/80)

Subtopic: programming as transformation up

Quote: for transformations, want the same language for specification, procedures, and assembly code; otherwise limits usefulness [»boylJM5_1999]
Quote: with a suitable programming language, would have an interactive program-manipulation system; like existing symbol-manipulation systems [»knutDE_1977]
Quote: program transformations should occur automatically after activation by the programmer [»baueFL_1976]
Quote: use syntactic and local semantic transformations to develop a program; e.g. to convert recursion to iteration [»arsaJJ1_1979]
Quote: use a catalogue of program transformations to simplify loop structure, eliminate nesting, etc. [»arsaJJ1_1979]

Subtopic: implementation as transformation up

Quote: the ultimate goal of programming language design is to express rubble programs which are automatically converted to efficient forms [»schwJT_1978]
Quote: commitment of representation decisions is the inverse of abstraction; program derivation is a sequence of commitments [»scheWL9_1983]
Quote: program refinements can be formalized by transformation rules with a source pattern, target pattern, and enabling condition [»smitDR11_1985]
Quote: start StreamBit with a reference program defining the task by its bit-level dataflow; then sketch a template for an efficient implementation [»solaA6_2005]
Quote: programming by sketches for rapid development; generate efficient code from clean, portable reference code by sketching the outlines of the desired implementation [»solaA6_2005]
Quote: given the same time budget, novice StreamBit users (sketching) produced 2.5x faster cipher code than experienced C coders; competitive implementations of DES and Serpent [»solaA6_2005]

Subtopic: specification to implementation up

Quote: use transformations of specifications to develop a program [»mannZ5_1978]
Quote: program design by transforming the specification's structure into a program structure; code the component parts; and combine into a system [»hoarCA9_1987]
Quote: with a transformational system, write software in a high-level specification language and transform it into an efficient program [»krueCW6_1992]
Quote: it is more natural to describe a program by its derivation or evolution from specifications [»scheWL9_1983]
Quote: transform a specification in a subject domain language to an equivalent description in the target language [»mannZ7_1979]
Quote: systematic coding from formal detailed design specifications; mapped Z specifications to code; pre- and post-conditions and invariants as assertions [»tretJ9_2001]

Subtopic: implementation to abstract up

Quote: create a abstract program or program schema by removing data typing and function definition [»elspB6_1972]

Subtopic: proof as transformation up

Quote: with an algebra, can prove theorems by mechanical transformations using algebraic laws [»backJ8_1978a]
Quote: RISC code is correct if the program is correct and you verify the transformations from program to RISC [»boylJM5_1999]
Quote: should separate program derivations from the process of building derivations [»scheWL9_1983]

Subtopic: optimization as transformation up

Quote: transform guarded regions into shorter equivalents; e.g., case structure to conditionals, or dropping a precondition that always holds [»brinP9_1978]
Quote: a machine-independent optimizer should be able to transform an inefficient program into a more efficient one with identical effects, expressed in the same language [»hoarCA_1974]
Quote: could use FP to transform a matrix multiply program which is space inefficient to efficient code [»backJ8_1978a]

Subtopic: debugging as transformation up

Quote: debug via a sequence of input/output transformations; at each stage verify the results [»leavBM7_1977]

Subtopic: structural equivalence up

Quote: program structures are path-wise convertible if they define the same sequence of primitive actions and predicates for every input [»ledgHF11_1975, OK]
Quote: program structures are semantically convertible if both compute the same function from the same set of primitive actions and predicates
[»ledgHF11_1975, OK]

Related Topics up

Topic: abstraction in programming (67 items)
Topic: code optimization by global analysis (24 items)
Topic: constructing proof and program together (22 items)
Topic: executable code from specifications and designs (18 items)
Topic: incremental development (74 items)
Topic: object slice (3 items)
Topic: object transformation language (10 items)
Topic: no need for efficiency (28 items)
Topic: programming as mathematics (27 items)
Topic: stepwise refinement (25 items)
Topic: string transformation languages (17 items)
Topic: structure transformation languages
(7 items)

Updated barberCB 3/05
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.