+ // By default, we will return true for @JustifyingPrecondition
+ code.addLine(TabbedLine(ShortComment("By default @JustifyingPrecondition returns true")));
+ code.addLine(TabbedLine("return true;"));
+
+ code.addLine("}");
+ code.addLine("");
+
+ }
+ // Define @JustifyingPostcondition
+ if (!construct.justifyingPostcondition.isEmpty()) {
+ code.addLine(ShortComment("Define @"
+ + SpecNaming.JustifyingPostcondition + " for " + name));
+ code.addLine("bool _" + name + "_" + SpecNaming.JustifyingPostcondition
+ + "(" + 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.justifyingPostcondition.align(1);
+ code.addLine(TabbedLine(ShortComment("Execute JustifyingPostcondition")));
+ code.addLines(construct.justifyingPostcondition);
+
+ // By default, we will return true for @JustifyingPostcondition
+ code.addLine(TabbedLine(ShortComment("By default @JustifyingPostcondition returns true")));