Technical Questions

[sagiv@haifasc3.vnet.ibm.com (Mooly Sagiv)]

We have just installed Centaur in Haifa scientific center and would like
to ask some questions.

Does anybody has a Metal specification of an abstract
and concrete syntax for C?

On the more conceptual level, we are now trying to use Centaur to
incorporate our semantics analysis. We want to analyze a PL-like
language. Our goal is to infer the type of the variables from their usage.
The natural candidate for this task is Typol.
Thus, we need to write type inference rules for our language.
However, these inference rules are not part of the language.
They are used to model software conventions.
This has the following impacts:
 a. The programmer will supply some of the type information
    by interaction with the type inference algorithm.
    This may be viewed as adding type definition for variables,
    on demand.
 b. There will be an interactive mode in which the programmer is
    asked to confirm the application of type inference rules.
 c. The programmer can add/delete inference rules, and regenerate
    the system.
 d. There may be more than one inference rule for a given program
    construct.
    For example, in the assignment x := y, there will be a number
    of rules using the type of x to infer the type of y and a number
    of rules to infer the type of x from y.
    A natural semantics for such inference rules is a fixed point
    semantics, i.e., inference rules will be applied till convergence
    in the symbol table occurs.

We suspect that Typol will be too high leveled to implement
these features and that some of the tasks need to be directly specified
using VTP. Are we right?

     Thanks, Mooly