loops - 如何使用 z3 验证循环？

Question

我是Z3的初学者。如何在 Z3 中验证具有循环不变量的循环（C 代码）？

例如：

int a[10],i;
for(i = 0; i<10; i++)
{    
  a[i] = 0;
}

Answer 1

Z3 仅支持带理论的一阶逻辑。您可以使用程序验证工具将带有断言的程序映射到逻辑。例如http://rise4fun.com/dafny或http://rise4fun.com/fstar。计算机科学中有关逻辑的合理课程还将包含有关如何编写验证条件生成器的材料。这些是这个问题的更好起点。