// have other name conflict
private String structName;
public final Code preCondition;
- public final Code justifyingCondition;
+ public final Code justifyingPrecondition;
public final Code transition;
+ public final Code justifyingPostcondition;
public final Code postCondition;
public final Code print;
this.name = null;
this.structName = null;
this.preCondition = new Code();
- this.justifyingCondition = new Code();
+ this.justifyingPrecondition = new Code();
this.transition = new Code();
+ this.justifyingPostcondition = new Code();
this.postCondition = new Code();
this.print = new Code();
*/
private Code generateAutoPrintFunction() {
Code code = new Code();
- // For RET
+ // For C_RET
code.addLines(SpecUtils.generatePrintStatement(funcHeader.returnType,
- SpecNaming.RET));
+ SpecNaming.C_RET));
// For arguments
for (VariableDeclaration decl : funcHeader.args) {
String type = decl.type;
if (!name.equals(SpecNaming.Interface)
&& !name.equals(SpecNaming.Transition)
&& !name.equals(SpecNaming.PreCondition)
- && !name.equals(SpecNaming.JustifyingCondition)
+ && !name.equals(SpecNaming.JustifyingPrecondition)
&& !name.equals(SpecNaming.SideEffect)
+ && !name.equals(SpecNaming.JustifyingPostcondition)
&& !name.equals(SpecNaming.PostCondition)
&& !name.equals(SpecNaming.PrintValue)) {
WrongAnnotationException.err(file, lineNum, name
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.JustifyingPrecondition)) {
+ this.justifyingPrecondition.addLines(primitive.contents);
+ } else if (name.equals(SpecNaming.JustifyingPostcondition)) {
+ this.justifyingPostcondition.addLines(primitive.contents);
} else if (name.equals(SpecNaming.PostCondition)) {
this.postCondition.addLines(primitive.contents);
} else if (name.equals(SpecNaming.PrintValue)) {