Re: Formal definitions

"Tim Frink" <plfriko@yahoo.de> wrote in message
> I'm looking for books/papers/websites where compiler optimizations
> are formally defined, i.e. not just textual and a code example.
> Any hints?


One answer is source-to-source program transformation systems, in
which pairs of target-language surface syntax patterns are written to
encode the transformation as a rewrite of the source text of the
program, e.g., pattern1 ==> pattern2


Stratego http://en.wikipedia.org/wiki/Stratego/XT and TXL
http://en.wikipedia.org/wiki/TXL_(programming_language) and Fermat
http://en.wikipedia.org/wiki/FermaT_Transformation_System are tools in
which such source-to-source transformations are entirely coded in
special rule langauges. Simple transformations that are context-free
can be coded directly. Taking into account context is harder and
requires cooperating sets of rules. Since rewrites are
generalizations of arbitrary string replaces, they are generalizations
of Post systems and thus can accomplish any transformation in theory.


Stratego and TXL can be applied to any langauge. Fermat is limited to
WSL, a language with formally defined semantics, but admits parsers
for other langauge that map to and from WSL.


Like Stratego and TXL,
DMS http://en.wikipedia.org/wiki/DMS_Software_Reengineering_Toolkit
has a rewrite rule language. However, it uses standard
compiler technology method to collect the context information
(symbol tables, control and data flow analyses) of
interest to transformations. Because context is so
important, as a practical matter,
many DMS transformations are written as
          pattern1 ==> pattern2 if condition
where the condition inspects some of the collected context
data. Similarly, rewrites aren't always a good
way to express transformations; DMS also
allows one to code complex transformations
procedurally (such as lambda lifting,
clone removal, ...)


Now transformations for a "compiler" are often from a programming
language level to a machine code level "langage". To the extent that
one can explicitly model both languages in the pattern language, it
can be handled directly by pattern rewriter. Stratego, TXL and DMS
can all do this easily. Stratego and TXL do this by allowing the
constructing a (joint) union grammar for source and target langauges,
with built in operators that compose grammars. DMS does this by
allowing disjoint unions of grammars so no grammer composition is
needed. One simply writes patterns in each of the languages and tags
the pattern according the grammar for which it applies.


One question that occurs over and over, is, "are the transformations
correct?" and "can you formally prove it?" Since the semantics of
the languages being transformed are not well-defined ina formal sense
(anybody seen denotational semantics for C++?) the answer to "can you
prove it" as a practical matter is outright NO. Are they correct?
Well, after rigourous testing, they are as correct as any other
program you might write. The Fermat system attempts to make
provability at least possible by insisting on the use of WSL, which is
formally defined. Of course, this simply pushes the burden on the
translator from your language X, which doesn't have formal semantics,
to WSL :-{


As an aside, I often get asked, "if you can't prove the
transformations correct, how you trust the tool?". My response is,
"if you aren't going to use a tool, then you going to use Joe to do
it, right? How can you trust Joe?".


--
Ira Baxter, CTO
www.semanticdesigns.com

Return to the comp.compilers page.
Search the comp.compilers archives again.