DAJ Examples

Semantic Checker

This is an example of a semantic checker for a system of simple equations. A more thorough treatment of the ideas behind DIs that also discuss this example can be found in our resent paper (under review).

For any system of equations, it is the case that any reference to a variable (or function name) is valid if and only if the variable (or function) has been previously defined. A semantic checker refers to the part of the program that verifies this property. The semantic checker needs to know of the different ways that variable (or functions) can be defined and also the different ways that variables (or functions) can be referred to.

As a first step, we will consider a simple equation system with variable definitions and no functions. Variables are defined when used as the left hand side of an equation, x = 5, and variables are referenced when they are used in the right hand side of an equation, y = x *5. From this description of how variables are being defined and used we can develop a DI for simple equation systems. 

        // ExprICG.di 
        di ExprICG with SemanticChecker{ 
          ESystem = List(Definition).
          Definition = <def> DThing "=" <body> Body. 
              Body = List(UThing).
              UThing = Thing. 
              DThing = Thing. 
              Thing = . 
              List(S) ~ "(" S ")". 
        }

The DI defines a general class dictionary expressing the notions required to define how variables are defined and used in a simple equation system. The next step is to define a traversal file that will operate on this DI. 

       // SemanticChecker.trv File 
        aspect SemanticChecker with DVisitor{
          declare strategy: gdefinedIdents: "from ESystem via DThing to Thing". 
          declare strategy: gusedIdents: "from ESystem via UThing to Thing".
          declare strategy definedIdent: "from Definition via DThing to Thing". 

          declare traversal: void printDefined(): gdefinedIdents(DVisitor); 
          declare traversal: void printUsed(): gusedIdents(DVisitor); 

          declare constraints: unique(definedIdent), nonempty(gusedIdents), nonempty(gdefinedIdents).
       }

The strategy gdefinedIdents navigates to all defined identifiers in the equation system, while definedIdent navigates form a definition to its only defined identifier. The restriction that there should be one unique identifier defined at each equation is expressed through the unique constraint. Finally, gusedIdents navigates to all locations where an identifier is used in the equation system. The nonempty constraints on gdefinedIdents and gusedIdents ensure that the adaptive code is applicable, i.e. there are some variables defined and thus the semantic checker is required to run. The definition of the DVisitor is given below. 

       // DVisitor.java File 
       class DVisitor {
         public void before(Thing t){
         System.out.println(t.toString());
         }
       }

The above definitions correspond to Phase I in docs. To complete the application we need to provide a concrete class dictionary that implements this DI and provides a valid mapping of the DI elements. 

         cd InfixEQSystem implements ExprICG {
           EquationSystem  = <eqs> List(Equation).
           List(S) ~ "(" {S} ")".
           Equation = <lhs> Variable "=" <rhs> Expr.
           Expr : Simple | Compound.
           Simple : Variable | Numerical.
           Variable = Ident.
           Numerical = <v> Integer.
           Compound = <lrand>List(Expr) <op> Op <rrand>List(Expr).
           Op : Add | Sub | Mul | Div.
           Add = "+".
           Sub = "-".
           Mul = "*".
           Div = "/".

           for ExprICG (
               EquationSystem as ESystem,
               use Equation as Definition,
               use Expr as Body,
               use (->*,lhs,Variable) as DThing,
               use (->*,rhs,* to Variable) as UThing, 
               use Variable as Thing
               )
         }

The class dictionary above defines a system of infix equations. The mapping provided defines the following correspondences (in order)

  • EquationSystem -> ESystem
  • Equation -> Definition
  • Any edge with the name lhs that points to a Variable -> DThing
  • Starting from any object that contains an edge named rhs and navigating to a Variable -> UThing
  • Variable -> Thing

We can run the code with the following Main class 

         import java.io.*;

          class Main { 
            public static void main(String[] args){
              try {
                InfixEQSystem ieqs = 
                InfixEQSystem.parse(new File(args[0]));
                System.out.println("IDs in def:");
                ieqs.printDefined();
                System.out.println("IDs in use:");
                ieqs.printUsed();
                }catch(Exception e){ 
                e.printStackTrace();
              }
            }
         }