// openjml --esc PostCondEx2.java
public class PostCondEx2 {

    public int divideByTwo(int num) {
        return num/2;
    }
}