Ключ изо всех сил пытается справиться с троичным оператором

Question

Я играю с KeY ( https://www.key-project.org/) для учебного проекта.

С одной стороны, я был счастлив, что KeY легко доказывает правильность следующего jml-аннотированного Java-кода.

/*@ ensures ((\result == a) || (\result == b));                                                                        
  @ ensures ((\result >= a) && (\result >= b));                                                                        
*/
public int max(int a, int b) {
    if(a <= b)
            return b;
    else
            return a;
}

но, с другой стороны, мне не удалось доказать правильность следующей эквивалентной программы

/*@ ensures ((\result == a) || (\result == b));                                                                        
  @ ensures ((\result >= a) && (\result >= b));                                                                        
*/
public int max(int a, int b) {
    return (a <= b) ? b : a;
}

Кто-нибудь знает, что я что-то упустил?

Answer 1

Спасибо за проверку Кей.

Приведенные примеры подтверждают автоматически с KeY 2.6.3 на моем компьютере. KeY имеет ряд настроек, от которых зависит механизм проверки. Возможно, некоторые из этих настроек делают KeY неудачным.

Вам нужно нажать кнопку "Выбрать Predef" на панели "Стратегия поиска пробных сообщений" и повторить попытку. Это должно работать тогда.

Вы можете также рассмотреть возможность удаления каталога ".key" в вашем домашнем каталоге, чтобы полностью сбросить настройки KeY. Возможно, некоторые настройки мешают работе инструмента.

Надеюсь это поможет!