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())
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);
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);
+ "),";
}
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