继续探讨: 有没有可以证明实际可用的语言?
我不知道你怎么看,但是我已经厌倦了编写无法保证质量的代码。
在提出以上问题并得到惊人回应后(感谢大家!),我决定将我的搜索范围缩小到一种可证明、实用、实用的方法,即Haskell。我选择 Haskell 是因为它实际上很有用(有许多Web框架用它编写,并且这似乎是一个很好的基准)而且我认为它在函数上足够严格,功能性很高,可能是可证明的,或者至少允许不变式测试。
以下是我想要的内容 (但一直没找到):
我想要一个框架,能够查看一个 Haskell 函数,添加如下伪代码:
add(a, b):
return a + b
- 并检查每个执行状态是否保持某些不变量。我希望有一些正式的证明,但如果有像模型检查器这样的东西,我也可以接受。在这个例子中,不变量将是给定值a和b时,返回值总是和a+b相等。
这是一个简单的例子,但我认为这样的框架存在并非不可能。显然,对于可测试的函数复杂度会有上限(例如,将10个字符串输入传递给一个函数肯定需要很长时间!),但这将鼓励更加谨慎地设计函数,并且与使用其他形式方法没有什么区别。想象一下在定义变量/集合时使用Z或B,您要确保变量的范围尽可能小。如果您的INT永远不会超过100,请确保将其初始化为此!诸如此类的技术以及适当的问题分解应该可以实现对Haskell这样的纯函数语言进行令人满意的检查。
我还不太熟悉形式化方法或Haskell。如果您认为我的想法是可行的,或者您认为Haskell不适合,那请告诉我。如果您建议使用其他语言,请确保它通过了“具有Web框架”测试,并阅读原始的问题 :-)