我正在通过关注their tutorial来试验why3，但我得到了多个证明者的消息 Unknown logical symbol map.Map.const . 以下是我试图证明的理论内容：
theory List
type list 'a = Nil | Cons 'a (list 'a)
predicate mem(x: 'a) (l: list 'a) = match l with
| Nil -> false
| Cons y r -> x = y || mem x r
end
goal G1: mem 2 (Cons 1 (Cons 2 (Cons 3 Nil)))
end
以下是各种证明的结果：
Z3：
▶ why3 prove -P z3 demo_logic.why
File "/usr/local/share/why3/drivers/z3_bare.drv", line 172, characters 36-41:
Unknown logical symbol map.Map.const
cvc4：
▶ why3 prove -P cvc4 demo_logic.why
File "/usr/local/share/why3/drivers/cvc4_bare.drv", line 180, characters 36-41:
Unknown logical symbol map.Map.const
PVS：
▶ why3 prove -P pvs demo_logic.why
File "/usr/local/share/why3/drivers/pvs-common.gen", line 41, characters 18-23:
Unknown logical symbol map.Map.const
这是我的3个版本信息：
▶ why3 --version
Why3 platform, version -n 0.85+git (build date: Tue Mar 10 08:27:47 EDT 2015)
错误消息中提到的.drv文件的时间戳与my3可执行文件的时间戳匹配 .
我的理论或安装有什么问题吗？
编辑添加：在教程本身它说使用 why3 demo_logic.why 来证明理论，但当我尝试我得到这个结果：
▶ why3 demo_logic.why
'demo_logic.why' is not a Why3 command.
如果我只是做 why3 prove demo_logic.why ，结果只是（近似）理论的回声：
▶ why3 prove demo_logic.why
theory List
(* use why3.BuiltIn.BuiltIn *)
type list 'a =
| Nil
| Cons 'a (list 'a)
predicate mem (x:'a) (l:list 'a) =
match l with
| Nil -> false
| Cons y r -> x = y || mem x r
end
goal G1 : mem 2 (Cons 1 (Cons 2 (Cons 3 (Nil:list int))))
end
1 回答
你安装了以前版本的why3吗？执行证明的问题通常是由于使用旧的why3的配置文件的新的why3 . 我已经看到你的特定实例由此修复：