The attributes
expr and
stats define successor nodes in the AST representation
, semantics defines the semantics
of
C-While in terms of
ASMs modeled by an external class
ASM.
Together this can be considered as an object-oriented definition
for the Montage [
KP97] in Figure 1. It defines
abstract syntax, control flow information (solid edges in the
graph), data flow information (dashed edges), and dynamic semantics
of the while loop.
I and T are used to integrate the statement
into its context. The dynamic semantics of the oval elements
(tasks of a certain type) is defined in the lower part of the
Montage. All together they define an interpreter using an abstract
program counter
ct. According to the rules computations
are performed and
ct is updated. The semantics of the
boxes must be defined by other Montages. These elements are plugged
in (using
I and
T) at the respective positions.
Hence, a Montage can be seen as a generic ASM definition of language
elements where the generic parameters (boxed elements) are itself
ASMs. For each syntactically correct program the Montages specification
of a language defines a task graph (tasks are nodes, control
and data flow information are edges). Its semantics is defined
by the interpreter described above.
Figure 2: Montage
for the AL while loop
In addition to this specification,
define describes the
transformation to the while statement of AL. which is
defined by the Montage in Figure 2 and is in turn represented
by a class AL-While. This transformation maps the
do command to the One command of AL, C-Stats
to AL-Stats and adapts C-IntExpr to AL-BoolExpr.
Therefore we introduce a wrapper that converts the result of
C-IntExpr to the required Boolean value. This wrapper
is defined in Figure 3. It is an instantiation of the Boolean
expression in AL which gets as a generic parameter an
AL-IntExpr. The C-IntExpr can now be mapped to
this AL-IntExpr. It can be proved that AL-While
together with the wrapped AL-IntExpr simulates C-While.
Figure 3: Wrapper
Int to Bool
Each transformation step has to be verified
by showing that the resulting ASM simulates the original one.
For each AL construct there exists either a transformation
to lower AL features which follows the same principles
as described above or a definition in terms of the intermediate
representation. However, the transformations within AL
are verified only once and can then safely be reused. The compiler
constructor needs only proof correct the transformation of the
source language to high level AL constructs.
References
[Gur95] Y. Gurevich
"Evolving Algebras: Lipari Guide",
Specification
and Validation Methods, Oxford University Press, 1995.
[KP97] P.W. Kutter and
A. Pierantonio "Montages: Specifications of Realistic Programming
Languages",
Journal of Universal Computer Science,
Vol. 3, Nr. 5, 1997.
Author contact: Institut für Programmstrukturen
und Datenorganisation, Universität Karlsruhe, Zirkel 2,
76128 Karlsruhe, Germany. Phone +49 721 608 7400. Fax: +49 721
30047. E-Mail: {heberle | loewe | trapp}@ipd.info.uni-karlsruhe.de.
