专门为使静态验证更容易而设计的语言
许多语言（也许所有）都是为了让编写程序变得更容易而设计的。它们都有不同的领域，并且旨在简化这些领域中的程序开发（C 使开发低级程序更容易，Java 使开发复杂的业务逻辑更容易等）。也许为了以更简单、更自然、更不易出错的方式编写和维护程序而牺牲了其他目的。
是否有专门设计的语言可以更轻松地验证源代码（即静态分析）？当然，为现代机器编写通用程序的能力也应该持续存在。
A lot of languages (perhaps all of them) are designed to make writing programs easier. They all have different domains, and aim to simplify developing programs in these domains (C makes developing low-level programs easier, Java makes developing complex business logic easier, et al.). Perhaps other purposes are sacrificed in sake of writing and maintaining programs in an easier, more natural, less error-prone way.
Are there any languages specifically designed to make verification of source code--i.e. static analysis--easier? Of course, capability to write common programs for modern machines should also persist.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（7）
Ada 的设计目标之一是支持一定数量的形式验证。取得了一定的成功，但验证并没有像他们希望的那样顺利进行。幸运的是，艾达的好处远不止于此。遗憾的是，这也没有多大帮助...
有一个名为 Spark 这使得它至今仍然存在。 Praxis 销售围绕其构建的开发套件。
One of the design goals of Ada was to support a certian amount of formal verification. It was moderately successful, but verification didn't exactly take off like they were hoping. Luckily Ada is good for far more than that. Sadly, that hasn't helped it much either...
There's an Ada subset called Spark that keeps this alive today. Praxis sells a development suite built around it.
这是 CLU 和 ML 语言的模糊目标，但据我所知，唯一真正认真对待静态验证的语言设计是 Spark Ada。
Dijkstra 的受保护命令语言（如《编程规则》中所述）旨在支持静态验证，但明确不应该实现它。
Gerard Holzmann 的 Promela 语言也是为模型检查器 SPIN 的静态分析而设计的，但同样它不可执行。
This was a vague goal of both the CLU and ML languages, but the only language design I know that takes static verification really seriously is Spark Ada.
Dijkstra's language of guarded commands (as described in Discipline of Programming) was designed to support static verification, but it was explicitly not supposed to be implemented.
Gerard Holzmann's Promela language was also designed for static analysis by the model checker SPIN, but again it's not executable.
E 语言中的审计器提供了一种在语言本身并要求某些代码部分通过一些静态检查。您可能还对本文的相关工作部分感兴趣。
Auditors in the E language provide a built-in means of writing code analyses within the language itself and requiring that some section of code pass some static check. You might also be interested in the related-work part of the paper.
我自己没有使用过它，所以我不能与任何权威交谈，但我知道 Eiffel 编程语言被设计为使用契约代码，这将使静态分析变得更加容易。我不知道这算不算。
I haven’t used it myself, so I can’t speak with any authority, but I understand that the Eiffel programming language was designed to use Code by Contracts, which would make static analysis much easier. I don’t know if that counts or not.
有 SAIL，静态分析中间语言或 Flexibo
There is SAIL, the Static Analysis Intermediate Language or Flexibo
“让源代码的验证变得更容易”有两个问题。一种是不做粗暴事情的语言，例如任意情况（例如 C）。
另一个是指定您想要验证的内容，为此您需要良好的断言语言。
虽然许多语言都提出了这样的断言语言，
我认为 EDA 社区一直在以时间规范最有效地挑战极限。 “属性规范语言”是一个标准；您可以通过P1850 PSL 标准：属性规范语言 (IEEE-1850) 了解更多信息。 PSL 背后的一个想法是您可以将其添加到现有的 EDA 语言中；我认为随着时间的推移，EDA 社区已经融入了 EDA 语言。
我经常希望将 PSL 这样的东西嵌入到传统的计算机软件中。
One has two problems in "making verification of source code easier". One is languages in which you don't do gross things such as arbitrary cases (such as C).
Another is specifying what you want to verify, for that you need a good assertions languages.
While many languages have proposed such assertions languages,
I think the EDA community has been pushing the envelope most effectively with temporal specifications. The "Property Specification Language" is a standard; you can learn more from P1850 Standard for PSL: Property Specification Language (IEEE-1850). One idea behind PSL is that you can add it to existing EDA languages; I think the EDA community has been incorporating into the EDA langauges as time goes by.
I've often wished for something like PSL to embed in conventional computer software.
静态验证对于这项任务来说是一个糟糕的开始。它基于这样一个假设：可以自动验证程序的正确性。这在现实世界中是不可行的，并且期望程序在没有任何提示的情况下检查任意复杂的代码简直是愚蠢的。通常，用于静态验证的软件最终需要在整个源代码中进行提示，并最终产生大量误报和漏报。它有一些利基市场，但仅此而已。 参阅 Pierce 对“类型和编程语言”的介绍）
（请 许多工具是工程师为了自己的简单目的而开发的，真正的解决方案已经在学院中烘焙出来。人们发现，如果一切顺利并且语言没有某种不良行为，静态类型编程语言中的类型相当于逻辑语句。这称为“Curry-Howard 对应”，并且嵌入逻辑类型为“Brouwer-Heyting-Kolmogorov 逻辑< /a>”。最强大的证明只有在具有强大类型的语言中才可能实现：依赖类型。如果我们暂时忘记所有这些术语，这意味着我们可以编写携带证明的程序 其自身的正确性，并且在程序编译时检查这些证明，并且在失败时不会给出可执行文件。
这种方法的积极的一面是你永远不会得到任何漏报，即保证编译的程序才能按照规范正常工作。即使没有关于规范的额外证明，依赖类型语言中的程序也不太容易出错，因为被零除、未处理的异常和溢出永远不会出现在可执行程序中。
总是用手写这样的证明是很乏味的。为此，有“策略”，即生成正确性证明的程序。这些几乎等同于静态验证程序，但与它们不同的是，它们需要生成形式证明。
有一系列用于不同目的的依赖类型语言：Coq、Agda, 伊德里斯，警句， Cayenne 等。
策略是在 Coq 和可能其他几种语言中实现的。 Coq 也是其中最成熟的，其基础设施包括 Bedrock 等库。
如果从 Coq 中提取的 C 代码不足以满足您的要求，您可以使用 ATS，其性能与 C 相当。
Haskell 采用 Curry 的弱形式-霍华德通信：它工作得很好，除非你开始编写失败或永远循环的程序。如果您的要求并不难编写正式证明，请考虑使用 Haskell。
Static verification is a bad start for this task. It's based on an assumption that it's possible to verify correctness of the program automatically. It's not feasible in real world, and expecting the program to check arbitrarily complex code without any hints is just plain dumb. Usually software for static verification ends up requiring hints all over source code, and in the end generates lots of false positives and false negatives. It has some niche, but that's it. (See introduction to "Types and programming languages" by Pierce)
While these kind of tools were developed by engineers for their own simple purposes, real solution have been baking in an academy. It was found that types in statically typed programming languages are equivalent to logic statements given everything goes smooth and language doesn't have some kind of bad behaviour. This is called "Curry-Howard correspondence", and the embedding of logic into types is "Brouwer-Heyting-Kolmogorov logic". The most powerful proofs are possible only in the languages with powerful types: dependent types. If we forget all this terminology for a while, this means that we can write programs that carry proofs of its own correctness, and these proofs are checked while the program gets compiled, with no executable file given in case of failure.
The positive side of this approach is that you never get any false negatives, i.e. compiled program is guaranteed to work properly according to the specification. Even without extra proofs about specification, programs in dependently-typed languages are less prone to mistakes, because divisions by zero, unhandled exceptions and overflows just never end up in an executable program.
Always writing such proofs by hand is tedious. For that there are "tactics", i.e. programs that generate proofs of correctness. These are almost equivalent to programs for static verification, but, unlike them, are required to generate formal proof.
There is a range of dependently-typed languages for different purposes: Coq, Agda, Idris, Epigram, Cayenne etc.
Tactics are implemented in Coq and probably several more languages. Also Coq is the most mature of them all, with infrastructure including libraries like Bedrock.
In case C code extraction from Coq is not enough for your requirements, you can use ATS, which is on par in performance with C.
Haskell employs weak form of Curry-Howard correspondence: it works fine, unless you start writing failing or forever-looping programs. In case your requirements are not that hard to write formal proofs, consider using Haskell.