我被教导关于正式系统 http://en.wikipedia.org/wiki/Formal_system在大学时，但我很失望它们似乎没有在现实世界中使用。
我喜欢这样的想法：能够知道某些代码（对象、函数等）是否有效，不是通过测试，而是通过proof.
我确信我们都熟悉物理工程和软件工程之间不存在的相似之处（钢铁的行为是可预测的，软件可以做任何事情——谁知道呢！），我很想知道是否有任何语言可以可以在实际应用中使用（对 Web 框架的要求是否过高？）
我听说过关于像 scala 这样的函数式语言的可测试性的有趣事情。
作为软件工程师我们有什么选择？
是的，有些语言是为编写可证明正确的软件而设计的。有些甚至用于工业。火花阿达 http://en.wikipedia.org/wiki/SPARK_%28programming_language%29可能是最突出的例子。我和 Praxis Critical Systems Limited 的一些人交谈过，他们使用它来在 Boings 上运行代码（用于引擎监控），它看起来相当不错。 （这里有一个很棒的语言的摘要/描述 http://cs.nyu.edu/courses/fall01/G22.3033-007/spintro.ppt.) 该语言和随附的证明系统使用下面描述的第二种技术。它甚至不支持动态内存分配！
我的印象和经验是，编写正确的软件有两种技术：
-
技术 1：用您熟悉的语言（例如 C、C++ 或 Java）编写软件。采用这种语言的正式规范，并证明您的程序是正确的。
如果您的目标是 100% 正确（这是汽车/航空航天行业最常见的要求），您将花费很少的时间进行编程，而花费更多的时间进行证明。
-
技术 2：用稍微尴尬的语言（例如 Ada 的某些子集或 OCaml 的调整版本）编写软件，并一路编写正确性证明。在这里，编程和证明是齐头并进的。在 Coq 中编程甚至完全等同于它们！ （参见库里-霍华德通信 http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence)
在这些情况下，您总是会得到正确的程序。 （错误肯定会根植于规范中。）您可能会在编程上花费更多时间，但另一方面，您会一路证明它的正确性。
请注意，这两种方法都取决于您手头有一个正式的规范（否则您如何判断什么是正确/不正确的行为），以及语言的正式定义的语义（您如何才能判断实际行为）你的程序是）。
以下是正式方法的更多示例。它是否是“现实世界”，取决于你问的是谁:-)
- Coq 定理证明者：使用 Coq 编程 http://www.labri.fr/perso/casteran/CoqArt/Tsinghua/C1.pdf（技巧2）
-
ESC/Java http://secure.ucd.ie/products/opensource/ESCJava2/（技术1，虽然不健全也不完整）
-
Spec# http://research.microsoft.com/en-us/projects/specsharp/（技术1，虽然不健全也不完整）
-
为什么/喀拉喀托 http://krakatoa.lri.fr/（技术2，基于Java）
我只知道一个“可证明是正确的”网络应用程序语言: UR http://www.impredicative.com/ur/。 “通过编译器”的 Ur 程序保证不会：
- 遭受任何类型的代码注入攻击
- 返回无效的 HTML
- 包含无效的应用程序内部链接
- HTML 表单与其处理程序期望的字段不匹配
- 包含对远程 Web 服务器提供的“AJAX”式服务做出错误假设的客户端代码
- 尝试无效的 SQL 查询
- 在与 SQL 数据库或浏览器和 Web 服务器之间的通信中使用不正确的编组和解组
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
