Если заявление с возвратом в JML

Question

Мне нужно установить постусловие, которое гарантирует возврат нуля, если size_ равен 0. На основании

 if(size_ == 0)
  return null;

как я могу сделать это в jml?есть идеи?Следующее не работает:

//@ ensures size_ == null ==> \return true;

заранее спасибо

Answer 1

Попробуйте

//@ ensures size_ == null ==> \result == true;

Пример:

//@ ensures size_ == null ==> \result == true;
public boolean sizeUndefined() {
    if (size_ == null)
        return true;

    return size_.length() > 0;
}

Вы также можете просто написать это так:

//@ ensures size_ == null ==> \result;

Вот документация для \result:

3.2.14 \result
В пределах нормального постусловия или цели модификации не пустого метода специальный идентификатор \ result является выражением спецификации, тип которого является типом возврата метода. Обозначает значение, возвращаемое методом. \ result допускается только в рамках прагмы обеспечивает, так же, как, либо изменяет, так и также: изменяет объявление не пустого метода.

Answer 2

Прежде всего: какой тип size_, Object или primitive(int)?

Во-вторых, каков тип возвращаемого метода? Object или primitive(boolean)?

Нельзя сравнивать тип примитива с null или возвращать null, если предполагается, что тип примитива должен быть возвращен. Если мы предположим, что size_ равно int, а возвращение boolean, то пост-условие будет

//@ ensures size_ == 0 ==> \result;