我正在查看自动化软件验证的要求,即,一个采用代码(用C和Java等语言编写的常规过程代码)的程序会生成一堆定理,说每个循环最终都必须停止,而不会违反任何断言,永远不会取消引用null指针等,然后将其传递给定理证明者以证明它们实际上是正确的(或者找到一个指示代码错误的反例)。
问题是要使用哪种逻辑。两个主要职位似乎是:
问题是,这两个职位似乎都有很多支持。那么哪一个是对的呢?如果是第二个,是否有任何您想做的事示例,基于一阶逻辑的验证程序会遇到麻烦?
最佳答案
您可以在FOL中完成所需的一切,但这需要大量的额外工作-很多!现有的大多数系统都是由学者/人员开发的,时间不多,因此很容易采取捷径来节省时间/精力,因此吸引了HOL,功能语言等。但是,如果您想构建一个我们相信FOL是必经之路,因为成千上万的人会使用它,而不仅仅是数百人。进行这项工作无可替代。我们已经有25年了!请看一下我们的项目(http://www.manmademinions.com)
问候,亚伦。
关于软件验证逻辑,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/3902684/