专门为使静态验证更容易而设计的语言

Ada的设计目标之一是支持一定数量的正式验证。这是相当成功的,但验证并没有像他们希望的那样成功。幸运的是,艾达做的远不止这些。可悲的是,这也没什么帮助。。。

有一个子集叫艾达 Spark 这让它今天还活着。 Praxis 销售围绕它构建的开发套件。

有没有专门设计的语言使源代码的验证更容易?

这是CLU和ML语言的一个模糊目标,但我知道唯一真正重视静态验证的语言设计是Spark Ada。

Dijkstra的戒备命令语言(如 程序设计学科 )它被设计来支持静态验证,但是它显然不应该被实现。

Gerard Holzmann的Promela语言也是为模型检查器SPIN的静态分析而设计的,但它同样是不可执行的。

Auditors 在E语言中,提供了一种在语言内部编写代码分析的内置方法,并要求某段代码通过一些静态检查。你也可能对论文的相关工作感兴趣。

我自己没有使用过它,所以我不能与任何权威人士交谈,但我知道,埃菲尔编程语言是按合同使用代码的,这将使静态分析更加容易。我不知道这算不算。

有 SAIL ,静态分析中间语言或 Flexibo

其中一个在“简化源代码验证”方面有两个问题。一种是语言,在这种语言中,你不会做一些粗俗的事情,比如任意的情况(比如C)。 另一个是 指定 你想验证的是,你需要一个好的断言语言。

虽然许多语言都提出了这样的断言语言, 我认为EDA社区一直在用时态规范最有效地推动这一进程。“属性规范语言”是一个标准;您可以从 P1850 Standard for PSL: Property Specification Language (IEEE-1850) . PSL背后的一个想法是,您可以将它添加到现有的EDA语言中,我认为随着时间的推移,EDA社区已经加入到EDA语言中。

我经常希望像PSL这样的东西嵌入到传统的计算机软件中。

静态验证对于这个任务来说是一个糟糕的开始。它基于一个假设,即可以自动验证程序的正确性。在现实世界中这是不可行的,期望程序在没有任何提示的情况下检查任意复杂的代码简直是愚蠢透顶。通常用于静态验证的软件在源代码中都需要提示,最终会产生大量的误报和漏报。它有一些利基,但就是这样。(见“简介” Types and programming languages “皮尔斯)

虽然这些工具是由工程师为自己的简单目的而开发的,但真正的解决方案一直在一所学院里酝酿。研究发现,静态类型编程语言中的类型与逻辑语句等价,因为一切都很顺利,而且语言没有任何不良行为。这叫做 Curry-Howard correspondence ,并且将逻辑嵌入到类型中是 Brouwer-Heyting-Kolmogorov logic ". 最有力的证明只有在具有强大类型的语言中才有可能: dependent types . 如果我们暂时忘记所有这些术语,这意味着我们可以 programs that carry proofs 其自身的正确性,这些证明在程序编译时进行检查,如果失败,则不提供可执行文件。

这种方法的积极一面是你永远不会得到任何 false negatives 也就是说,保证编译后的程序按照规范正常工作。即使没有关于规范的额外证明,依赖类型语言中的程序也不太容易出错,因为零除、未处理的异常和溢出永远不会在可执行程序中结束。

总是用手写这样的证明是乏味的。为了这个 tactics ,即生成正确性证明的程序。它们几乎等同于用于静态验证的程序,但与它们不同的是,它们需要生成正式的证明。

有一系列用于不同目的的独立类型语言: Coq , Agda , Idris , Epigram , Cayenne 等。

战术是用Coq和其他几种语言实现的。Coq也是其中最成熟的,它的基础设施包括 Bedrock .

如果从Coq中提取的C代码不足以满足您的需求,您可以使用 ATS ,这在性能上与C相当。

Haskell 使用弱形式的Curry-Howard通信:它工作得很好,除非你开始编写失败或永远循环的程序。如果您的需求不是那么难写正式的证明,考虑使用Haskell。