public class Calculator { private int result; public Calculator() { result = 0; } public void add(int number) { //@requires("number > 0") //@ensures("result == \\old(result) + number") result += number; } public int getResult() { //@ensures("result >= 0") return result; } }