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

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.

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

Вам следует нажать кнопку «Выбрать Predef» на панели «Стратегия поиска доказательства» и повторить попытку.Тогда он должен работать.

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

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