-
2 votesanswersviews
将WhyML映射到SMT逻辑的确切机制
美好的一天，自动扣除和验证黑客！ 为了更深入地了解WhyML究竟如何为ACSL注释的C程序提供证据，我试图手动“重现”Why3对WhyML程序的工作，同时将其转换为SMT逻辑并将其提供给Z3证明器 . 假设我们有以下C片段： const int L = 3; int a[L] = {0}; int i = 0; while (i < L) { a[i] = i; i++; } ass... -
0 votesanswersviews
在Why3中'Unknown logical symbol map.Map.const'消息
我正在通过关注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 wi... -
2 votesanswersviews
如何在coq中证明why3生成的脚本？
我使用frama-C WP并想调试我的ACSL注释（理解为什么说服者说我“不知道”） . 我有一些绿色或橙色的结果 . 我打开why3 IDE并查看生成的脚本 . 然后我从列表中选择一个理论/目标，并能够启动Alt-Ergo或Coq IDE . 我想在Coq IDE中使用生成的代码 . 我看到一些公理然后定理WP，然后，例如： intros a a_1 i_3 i_2 i_1 i t_2 t_1 ...