edits

[cdsspec-compiler.git] / src / edu / uci / eecs / specExtraction / InterfaceConstruct.java

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)) {