edits

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
index 7dcaaa0acec7a605c3bedca3858964d6a9bb6e47..6a90a72eec1f286786f847cb945124cee8eb6707 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
@@ -408,6 +408,15 @@ public class CodeGeneratorUtils {
                                        code.addLine(DeclareDefine(SpecNaming.CString,
                                                        SpecNaming.AppendStr(tmpFunc),
                                                        SpecNaming.EmptyCString));
+                               // JustifyingCondition
+                               tmpFunc = name + "_" + SpecNaming.JustifyingCondition;
+                               if (!construct.justifyingCondition.isEmpty())
+                                       code.addLine(DeclareDefine(SpecNaming.CString,
+                                                       SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+                               else
+                                       code.addLine(DeclareDefine(SpecNaming.CString,
+                                                       SpecNaming.AppendStr(tmpFunc),
+                                                       SpecNaming.EmptyCString));
                                // PostCondition
                                tmpFunc = name + "_" + SpecNaming.PostCondition;
                                if (!construct.postCondition.isEmpty())
@@ -594,13 +603,14 @@ public class CodeGeneratorUtils {
                                if (!construct.preCondition.isEmpty()) {
                                        code.addLine(ShortComment("Define @"
                                                        + SpecNaming.PreCondition + " for " + name));
-                                       code.addLine("bool _" + name + "_"
-                                                       + SpecNaming.PreCondition + "(" + SpecNaming.Method
-                                                       + " " + SpecNaming.Method1 + ") {");
+                                       code.addLine("bool _" + name + "_" + SpecNaming.PreCondition
+                                                       + "(" + SpecNaming.Method + " " + SpecNaming.Method1
+                                                       + ", " + SpecNaming.Method + " " + SpecNaming.Method2
+                                                       + ") {");
 
                                        // Initialize value struct fields
                                        fieldsInit = GenerateInterfaceFieldsInitialization(
-                                                       SpecNaming.Method1, SpecNaming.InterfaceValueInst,
+                                                       SpecNaming.Method2, SpecNaming.InterfaceValueInst,
                                                        construct);
                                        fieldsInit.align(1);
                                        code.addLines(fieldsInit);
@@ -616,19 +626,47 @@ public class CodeGeneratorUtils {
                                        code.addLine("}");
                                        code.addLine("");
 
+                               }
+                               // Define @JustifyingCondition
+                               if (!construct.justifyingCondition.isEmpty()) {
+                                       code.addLine(ShortComment("Define @"
+                                                       + SpecNaming.JustifyingCondition + " for " + name));
+                                       code.addLine("bool _" + name + "_" + SpecNaming.JustifyingCondition
+                                                       + "(" + SpecNaming.Method + " " + SpecNaming.Method1
+                                                       + ", " + SpecNaming.Method + " " + SpecNaming.Method2
+                                                       + ") {");
+
+                                       // Initialize value struct fields
+                                       fieldsInit = GenerateInterfaceFieldsInitialization(
+                                                       SpecNaming.Method2, SpecNaming.InterfaceValueInst,
+                                                       construct);
+                                       fieldsInit.align(1);
+                                       code.addLines(fieldsInit);
+
+                                       construct.justifyingCondition.align(1);
+                                       code.addLine(TabbedLine(ShortComment("Execute JustifyingCondition")));
+                                       code.addLines(construct.justifyingCondition);
+
+                                       // By default, we will return true for @PreCondition
+                                       code.addLine(TabbedLine(ShortComment("By default @JustifyingCondition returns true")));
+                                       code.addLine(TabbedLine("return true;"));
+
+                                       code.addLine("}");
+                                       code.addLine("");
+
                                }
                                // Define @PostCondition
                                if (!construct.postCondition.isEmpty()) {
                                        code.addLine(ShortComment("Define @"
                                                        + SpecNaming.PostCondition + " for " + name));
-                                       code.addLine("bool _" + name + "_"
-                                                       + SpecNaming.PostCondition + "("
-                                                       + SpecNaming.Method + " " + SpecNaming.Method1
+                                       code.addLine("bool _" + name + "_" + SpecNaming.PostCondition
+                                                       + "(" + SpecNaming.Method + " " + SpecNaming.Method1
+                                                       + ", " + SpecNaming.Method + " " + SpecNaming.Method2
                                                        + ") {");
 
                                        // Initialize value struct fields
                                        fieldsInit = GenerateInterfaceFieldsInitialization(
-                                                       SpecNaming.Method1, SpecNaming.InterfaceValueInst,
+                                                       SpecNaming.Method2, SpecNaming.InterfaceValueInst,
                                                        construct);
                                        fieldsInit.align(1);
                                        code.addLines(fieldsInit);
@@ -791,6 +829,20 @@ public class CodeGeneratorUtils {
                                                        + "),";
                                }
                                code.addLine(TabbedLine(line, 2));
+                               // JustifyingCondition
+                               line = "new "
+                                               + SpecNaming.NamedFunction
+                                               + "("
+                                               + SpecNaming.AppendStr(name + "_"
+                                                               + SpecNaming.JustifyingCondition) + ", "
+                                               + SpecNaming.JustifyingConditionType + ", (void*) ";
+                               if (construct.justifyingCondition.isEmpty()) {
+                                       line = line + SpecNaming.NullFunc + "),";
+                               } else {
+                                       line = line + "_" + name + "_" + SpecNaming.JustifyingCondition
+                                                       + "),";
+                               }
+                               code.addLine(TabbedLine(line, 2));
                                // PostCondition
                                line = "new "
                                                + SpecNaming.NamedFunction

diff --git a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
index 1ff0cb05514cc3c8e7c01d56587cee307c6bcd03..e2b0290685bd0c2d4cedac92383b53330423b029 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
+++ b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
@@ -30,6 +30,7 @@ public class InterfaceConstruct extends Construct {
        // have other name conflict
        private String structName;
        public final Code preCondition;
+       public final Code justifyingCondition;
        public final Code transition;
        public final Code postCondition;
        public final Code print;
@@ -53,6 +54,7 @@ public class InterfaceConstruct extends Construct {
                this.name = null;
                this.structName = null;
                this.preCondition = new Code();
+               this.justifyingCondition = new Code();
                this.transition = new Code();
                this.postCondition = new Code();
                this.print = new Code();
@@ -122,6 +124,7 @@ public class InterfaceConstruct extends Construct {
                if (!name.equals(SpecNaming.Interface)
                                && !name.equals(SpecNaming.Transition)
                                && !name.equals(SpecNaming.PreCondition)
+                               && !name.equals(SpecNaming.JustifyingCondition)
                                && !name.equals(SpecNaming.SideEffect)
                                && !name.equals(SpecNaming.PostCondition)
                                && !name.equals(SpecNaming.PrintValue)) {
@@ -178,6 +181,8 @@ public class InterfaceConstruct extends Construct {
                                this.transition.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.PreCondition)) {
                                this.preCondition.addLines(primitive.contents);
+                       } else if (name.equals(SpecNaming.JustifyingCondition)) {
+                               this.justifyingCondition.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.PostCondition)) {
                                this.postCondition.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.PrintValue)) {

diff --git a/src/edu/uci/eecs/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
index df0b5f1cb78d5c1928d6d49796e01274a604bf9a..f8925fbd0d7fb1a2d8f42c21e4874bd4911031a8 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecExtractor.java
+++ b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
@@ -624,7 +624,7 @@ public class SpecExtractor {
                        lineReader = new LineNumberReader(br);
                        // "/\*\*\s*@(DeclareState|Interface)"
                        Pattern regexpBegin = Pattern
-                                       .compile("/\\*\\*\\s*@(DeclareState|Interface|PreCondition|Transition|PostCondition|Define)");
+                                       .compile("/\\*\\*\\s*@(DeclareState|Interface|PreCondition|JustifyingCondition|Transition|PostCondition|Define)");
                        Matcher matcher = regexpBegin.matcher("");
 
                        String line;
@@ -654,6 +654,7 @@ public class SpecExtractor {
                                                                beginLineNum);
                                        } else if (constructName.equals(SpecNaming.Interface)
                                                        || constructName.equals(SpecNaming.PreCondition)
+                                                       || constructName.equals(SpecNaming.JustifyingCondition)
                                                        || constructName.equals(SpecNaming.Transition)
                                                        || constructName.equals(SpecNaming.PostCondition)) {
                                                extractInterfaceConstruct(file, lineReader, line,

diff --git a/src/edu/uci/eecs/specExtraction/SpecNaming.java b/src/edu/uci/eecs/specExtraction/SpecNaming.java
index 8355b75fc696b2d7a0fa5fd11e6f3661b41dbcec..5b48c99faf6fb95874a680e498cf61d10e1233c2 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecNaming.java
+++ b/src/edu/uci/eecs/specExtraction/SpecNaming.java
@@ -33,6 +33,7 @@ public class SpecNaming {
        public static final String Interface = "Interface";
        public static final String Transition = "Transition";
        public static final String PreCondition = "PreCondition";
+       public static final String JustifyingCondition = "JustifyingCondition";
        public static final String SideEffect = "SideEffect";
        public static final String PostCondition = "PostCondition";
        public static final String PrintValue = "Print";
@@ -41,6 +42,7 @@ public class SpecNaming {
        public static final String PrintValueType = "PRINT_VALUE";
        public static final String TransitionType = "TRANSITION";
        public static final String PreConditionType = "PRE_CONDITION";
+       public static final String JustifyingConditionType = "JUSTIFYING_CONDITION";
        public static final String SideEffectType = "SIDE_EFFECT";
        public static final String PostConditionType = "POST_CONDITION";