Как написать спецификацию OpenJML?

Question

Мне нужно реализовать спецификацию для пары методов моей домашней работы. Я провел небольшое исследование в Интернете и прочитал документацию, и все, что я обнаружил, это то, что в основном речь идет о добавлении предварительных и пост-условий. Но методы, для которых должна быть реализована спецификация, выглядят так

// @ requires element > 0 && elements < CAPACITY && size >= && size <= CAPACITY;
    // @ ensures \result ==(\exists int i; 0 <= i && i < getSize(); data[i] == element);
    public /*@ pure @*/ boolean contains(int element) {
        int i = 0;
        //@ loop_invariant i >= 0 ;
        for (; i < size; i++)
            //@assume i < data.length ;
            if (data[i] == element)
                return true;
        return false;
    }

Что меня сбило с толку, так это то, что если пост- и предварительные условия уже были, что мне делать и как?