VIATRA2/Examples/VTCL/TypeChecking

From Eclipsepedia

< VIATRA2‎ | Examples‎ | VTCL
Jump to: navigation, search

Contents

Overview: Type checking

Type checking is introduced to the VTCL language in a backward compatible way. This means that any existing VTCL transformation should compile without modification. Moreover, it also implies that detailed type checking is only initiated if a type is defined explicitly for a variable (or an ASM function).

As the main extension of the language, one can add type information to

  • all variables defined locally with the let rule
  • a parameter of an ASM rule, graph pattern or graph transformation rule
  • for the parameters and return values of ASM functions

Then the VIATRA2 parser checks if these variables are used in a type conformant way.

Typed variables within ASM rules

In ASM rules, types can be assigned to variables within the let rule with the following syntax VarName : TypeConst = InitValue. Here the type constant TypeConst should be a valid element of the model space, which can be resolved at compile time.

The following example demonstrates two typical type errors identified by the typechecker.

 machine typechecking_errors {
   rule main() = 
   let X : datatypes.Integer = 0, 
       // Type error: Type incompatible initialization: expecting a term of type 'Integer' instead of 'String'	
       Y : datatypes.Integer = "oops0"
   in
     seq {
           // Type error: operation '*' undefined for types ('Integer', 'String') 
  	  update X = X * "oops1";
           // Type error: type incompatible assignment: left value is of type 'Integer', right value is of type 'String'
  	  update X = X + "oops2";
           // This is correct
  	  update X = X + 3;	  
     }
 }

In case of user defined ASM rules, types may be attached to symbolic parameters of the rule with the following syntax: Dir VarName : TypeConst where Dir denotes the direction of the parameter (i.e. it is either in, out or inout).

TODO: Maybe, the following example should not be a type error

   rule calledAsmRule(in X: datatypes.Integer, out Y: datatypes.Double) = seq {
   	update Y = 2 * X;
   }
   rule typecheck_asmrule() = 
   let X : datatypes.Integer = 2, Y : datatypes.Integer = 0 in 
     seq {
         // Type error: The type 'Integer' of actual parameter is not compatible with the type 'Double' of symbolic parameter 'Y'. 
         // See the definition of 'calledAsmRule'.
   	  call calledAsmRule(X, Y);
     }

Important: Since type declarations for variables are optional, the typing of symbolic parameter lists (or variable declarations with let) are different from the Java convention, i.e. if no type is indicated for a variable in a symbolic parameter list then it is not explicitly typed. For instance,

 let X = 2, Y : datatypes.Integer = 0 in ... // Y is typed, X is untyped
 rule calledAsmRule(in X, out Y: datatypes.Double) = ... // Y is typed, X is untyped

Typed variables in ASM functions

In case of ASM functions, types can be defined (separately) for each parameter (location) as well as for the return value with the following syntax:

asmfunction myFun (TypeConst1, TypeConst2) : ReturnTypeConst

 machine typecheck_asmfun {
  asmfunction goals(datatypes.String) : datatypes.Integer  {
        // Correct initialization
	  ("Messi") = 3;
        // Type error (left value): type incompatible initialization: expecting a term of type 'String' instead of type 'Integer'
        // Type error (right value): type incompatible initialization: expecting a term of type 'Integer' instead of type 'String'
  	(3) = "Giggs";
  }
  rule main () = let X : datatypes.Integer = 0, Y : datatypes.String = "Giggs" in seq {
       // Correct assignment
       update X = goals("Messi");
       // Type error: Type incompatible assignment: left value is of type 'String', right value is of type 'Integer'
       update Y = goals("Messi");
       // Correct assignment
       update goals(Y) = 2; 
       // Type error: Type incompatible initialization: expecting a term of type 'String' instead of type 'Integer'
       update goals(X) = 2; 	  
  }
 }

Typed variables in graph patterns

In case of graph patterns, there are two kinds of type definitions for pattern variables:

  • Types of symbolic parameters: This is defined similarly to the type definition in case of ASM rules, i.e. X: Class.
  • Pattern body elements: the type of pattern variables defined within a pattern body is defined by the prefixing type constant. For instance, the type X in Class(X) is, obviously, Class.

The following situations are typechecked:

  • a pattern is called with incompatible types (see find childPattern(P) below)
  • the type of a pattern body element is incompatible with the type of the symbolic parameter (see X: Class and Classifier(X) below)


   pattern myPattern(X: Class, Y: Classifier) = 
   {
        // Type error for X: The type 'Classifier' of variable reference is not compatible with the type 'Class' of its definition.	
   	Classifier(X);
        // Type error for X: The type 'Classifier' of variable reference is not compatible with the type 'Class' of its definition.	
 	  Element.ownedElement(OE1, P, X);
   	Package(P);
        // The type 'Package' of actual parameter is not compatible with the type 'Classifier' of symbolic parameter 'A'. 
        // See the definition of 'childPattern1'.
 	  find childPattern1(P);
        // The type 'Package' of actual parameter is not compatible with the type 'Class' of symbolic parameter 'A'. 
        // See the definition of 'childPattern2'.
   	find childPattern2(P);
   	Element.ownedElement(OE2, P, Y);
   	Class(Y);
   }   
   
   pattern childPattern1(A: Classifier) = 
   { 
   	Class(A);
   } 
   
   pattern childPattern2(A) = 
   { 
   	Class(A);
   } 

Note that the type of a pattern variable is infered (if possible) from the local pattern body elements. Therefore, an error message is reported when calling childPattern2 with an incorrectly typed parameter P as the symbolic parameter A of childPattern2 is typed implicitly by the pattern body Class(A).

Error messages

The following error messages are issued by the type checker. Note that currently, these messages are classified as warnings!

  • Operator '-' is undefined for the argument type ('datatypes.String'): issued when checking an ASM term
  • Operator '*' is undefined for the argument types ('datatypes.String', 'datatypes.String'): issued when checking an ASM term
  • The type 'uml2.metamodel.Classifier' of actual parameter is not compatible with the type 'uml2.metamodel.Class' of symbolic parameter 'C'. See the definition of 'myPattern' : issued when calling a graph pattern using the find construct
  • The type 'uml2.metamodel.Classifier' of variable reference is not compatible with the type 'uml2.metamodel.Class' of its definition.: issued in ASM rules or in the body of graph patterns
  • Type incompatible assignment: left value is of type 'datatypes.String', right value is of type 'datatypes.Integer' : issued in case of an update rule
  • Type incompatible initialization: expecting a term of type 'datatypes.String' instead of 'datatypes.Integer' : issued when initializing an ASM function

--Varro.mit.bme.hu 11:02, 25 May 2009 (UTC)