专门设计用于简化静态验证的语言

P S*_*ved 17 programming-languages static-analysis

很多语言(可能都是这些语言)旨在使编写程序更容易.它们都有不同的领域,旨在简化这些领域的开发程序(C使开发低级程序更容易,Java使开发复杂的业务逻辑更容易,等等).为了以更容易,更自然,更不容易出错的方式编写和维护程序,可能会牺牲其他目的.

是否有任何专门用于验证源代码的语言 - 即静态分析 - 更容易?当然,为现代机器编写通用程序的能力也应该持续存在.

T.E*_*.D. 5

Ada的设计目标之一是支持大量的正式验证.它取得了一定程度的成功,但验证并没有像他们希望的那样完全起飞.幸运的是,阿达的好处远不止于此.可悲的是,这对它没有多大帮助......

有一个名为Spark的Ada子集,它可以保持这种活力.Praxis销售围绕它构建的开发套件.