ほぼ完成しました。前回紹介したのとほぼ変わってませんが・・・こんな感じで書けます。@Invariant(enableds={true, true})@PreCondition(exps={"$1.doubleValue() == 10", "$2.intValue() > 0"})@PostCondition(exps={"$1.doubleValue() == 10", "$2.intVal…