IMPLEMENTATION MODULE MetrGPreconditions;

FROM YaflGCode         IMPORT GC;
FROM YaflType          IMPORT TypedNonTerminal;
FROM Streams           IMPORT StdOut;
FROM YaflCfg           IMPORT YaflCfg;
FROM YaflDesignator    IMPORT Desig;
FROM YaflPredefined    IMPORT PredefNoChangeMethod;
FROM YaflModules       IMPORT CompilationUnit;
FROM YaflClasses       IMPORT ClassDeclaration;
FROM YaflMethods       IMPORT MethodDeclaration, 
                              Formal,
                              FormalList;
FROM YaflPreconditions IMPORT Assertion,
                              PreCondition,
                              PostCondition,
                              Invariant,
                              ClassInvariant,
                              LoopInvariant,
                              MethodAssertion,
                              OldExpression,
                              UniversalQuantifierExpression,
                              ForAllExpression,
                              ThereIsExpression;
FROM YaflAsGC          IMPORT AssertionGC;                     
                              
                              
   CLASS MetrPreCondCodeGenerator;
     INHERITS PreCondCodeGenerator(CGcContext);
     
   END MetrPreCondCodeGenerator;

----------------------------------------------------------

   CLASS MetrPostCondCodeGenerator;
     INHERITS PostCondCodeGenerator(CGcContext);
   
   END MetrPostCondCodeGenerator;

----------------------------------------------------------

   CLASS MetrClassInvCodeGenerator;
     INHERITS ClassInvCodeGenerator(CGcContext);
   
   END MetrClassInvCodeGenerator;

----------------------------------------------------------

   CLASS MetrLoopInvCodeGenerator;
     INHERITS LoopInvCodeGenerator(CGcContext);
   
   END MetrLoopInvCodeGenerator;

----------------------------------------------------------

   CLASS MetrForAllExprCodeGenerator;
     INHERITS ForAllExprCodeGenerator(CGcContext);
     
   END MetrForAllExprCodeGenerator;
   
----------------------------------------------------------

   CLASS MetrThereIsExprCodeGenerator;
     INHERITS ThereIsExprCodeGenerator(CGcContext);
     
   END MetrThereIsExprCodeGenerator;
   
----------------------------------------------------------

   CLASS MetrOldExprCodeGenerator;
     INHERITS OldExprCodeGenerator(CGcContext);
     
   END MetrOldExprCodeGenerator;
     
END MetrGPreconditions;

