小编use*_*302的帖子

我正在与 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 …