Fares Fraij, 12/3/03
A Framework for Verifying HATS
Abstract: The High-Assurance Transformation system (HATS) is a language
independent program transformation system whose goal is to provide a
transformation-oriented programming environment facilitating the
development of transformation rules and strategies whose correctness can
be formally verified. In HATS, programs are defined by a context-free
grammar. These programs are manipulated internally as Syntax Derivation
Trees (SDT). HATS manipulate the SDTs by transformation rules and
strategies, which are defined using a special purpose language. The
output is also an SDT that results from applying the transformation
rules (TR) to the input SDT according to a control strategy. The goal of
our work is to prove that the application of these transformation rules
and strategies preserves semantics.
Our modeling and verification framework of the transformation system
(HATS) is similar to the framework that was adapted in verifying parts
of the implementations of the JVM. Our model consists of a state and a
state transition function. The state consists an SDT, a control
operator, a transformation sequence, and two Program counters (PCs), one
to keep track of the next transformation rule (TR) to be applied and the
other to keep track of the next node to apply the TR to, respectively.
The transition function is the function that takes the current state and
returns a new state that results from applying the current TR.
We start with the control operator "once" that applies the
transformation sequence one time per node and traverses the SDT one
time. We are trying to apply "once" in a top-down fashion. Thereafter,
we can go on and model some other control operators that were added in
the recent version of HATS. For the verification part, we will use
simple arithmetic expressions since we can obtain semantics function for
such expressions. The verification effort will be to show that the TR
preserves the meaning