- // Declare @Initial
- code.addLine(ShortComment("Declare @" + SpecNaming.InitalState));
- code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "(" + SpecNaming.Method + " "
- + SpecNaming.Method1 + ");");
- code.addLine("");
- // Declare @Copy
- code.addLine(ShortComment("Declare @" + SpecNaming.CopyState));
- code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "(" + SpecNaming.Method + " " + "dest, "
- + SpecNaming.Method + " src);");
- code.addLine("");
- // Declare @Print
- code.addLine(ShortComment("Declare @" + SpecNaming.PrintState));
- if (!globalConstruct.printState.isEmpty()) {
- code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "(" + SpecNaming.Method + " "
- + SpecNaming.Method1 + ");");
- code.addLine("");
- }
-
- // Declare @Commutativity
- code.addLine(ShortComment("Declare commutativity checking functions"));
- for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
- code.addLine("bool _check" + SpecNaming.Commutativity + i + "(" + SpecNaming.Method + " m1, "
- + SpecNaming.Method + " m2);");
- }
- code.addLine("");
-
- // Declare customized interface functions
- for (File file : interfaceListMap.keySet()) {
- ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
- for (InterfaceConstruct construct : list) {
- // Declare interface functions
- String name = construct.getName();
- code.addLine("/********** " + name + " functions **********/");
- // Declare @Transition for INTERFACE
- code.addLine(ShortComment("Declare @" + SpecNaming.Transition + " for " + name));
- code.addLine("void _" + name + "_" + SpecNaming.Transition + "(" + SpecNaming.Method + " "
- + SpecNaming.Method1 + ", " + SpecNaming.Method + " " + SpecNaming.Method2 + ");");
- code.addLine("");
- // Declare @PreCondition
- if (!construct.preCondition.isEmpty()) {
- code.addLine(ShortComment("Declare @" + SpecNaming.PreCondition + " for " + name));
- code.addLine("bool _" + name + "_" + SpecNaming.PreCondition + "(" + SpecNaming.Method + " "
- + SpecNaming.Method1 + ");");
- code.addLine("");
- }
- // Declare @SideEffect
- if (!construct.sideEffect.isEmpty()) {
- code.addLine(ShortComment("Declare @" + SpecNaming.SideEffect + " for " + name));
- code.addLine("void _" + name + "_" + SpecNaming.SideEffect + "(" + SpecNaming.Method + " "
- + SpecNaming.Method1 + ");");
- code.addLine("");
- }
- // Declare @PostCondition
- if (!construct.postCondition.isEmpty()) {
- code.addLine(ShortComment("Declare @" + SpecNaming.PostCondition + " for " + name));
- code.addLine("bool _" + name + "_" + SpecNaming.PostCondition + "(" + SpecNaming.Method + " "
- + SpecNaming.Method1 + ");");
- code.addLine("");
- }
- // Declare @Print
- if (!construct.print.isEmpty()) {
- code.addLine(ShortComment("Declare @" + SpecNaming.PrintValue + " for " + name));
- code.addLine("void _" + name + "_" + SpecNaming.PrintValue + "(" + SpecNaming.Method + " "
- + SpecNaming.Method1 + ");");
- code.addLine("");
- }
- }
- }
-