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