Coq:无法在加载路径中找到库Jessie_memory_model

Question

运行以下命令frama-c -jessie max-anno.c后，GUI正确启动，但在运行Coq时，我得到以下输出：

Welcome to Coq 8.4pl4 (July 2014)
Warning: Cannot open /usr/local/lib/why3/coq-tactic
File "/tmp/why_d206da_maxmnanno_T_WP_parameter_max_ensures_default.v", line 9, characters 0-28:
Error: Cannot find library Jessie_memory_model in loadpath
why3cpulimit time : 1.000000 s

麦克斯-阿诺特：

/*@ ensures \result >= x && \result >= y;
    ensures \result == x || \result == y;
*/
int max(int x, int y) { return (x > y) ? x : y; }

这个问题的截图：

​

​

似乎缺少"Jessie_memory_model“，但我不知道如何获得它，也不知道在哪里安装它。

编辑: why3版本为0.83。

Answer 1

why3的0.83版本不支持coq8.4。试着安装其他的测试器。我安装了Alt和CVC3.