0at*_*man 50 java testing formal-verification functional-programming scala
我在大学里接受过有关正式系统的教学,但我很失望,他们似乎并没有在真正的单词中使用它们.
我喜欢能够知道某些代码(对象,函数,等等)可以工作的想法,而不是通过测试,而是通过证明.
我确信我们都熟悉物理工程和软件工程之间不存在的相似之处(钢铁行为可预测,软件可以做任何事情 - 谁知道!),我很想知道是否有任何语言可以在真实的单词中使用(要求Web框架太多要问？)
我听说过像scala这样的函数式语言的可测试性.
作为软件工程师我们有什么选择？
aio*_*obe 35
是的,有一些语言专为编写可证明正确的软件而设计.有些甚至用于工业.Spark Ada可能是最突出的例子.我和Praxis Critical Systems Limited的一些人谈过,他们用它来运行Boings上的代码(用于引擎监控),看起来相当不错.(这是对语言的一个很好的总结/描述.)这种语言和随附的证明系统使用下面描述的第二种技术.它甚至不支持动态内存分配!
我的印象和经验是,有两种编写正确软件的技巧:
技巧1:用您熟悉的语言编写软件(例如C,C++或Java).采用这种语言的正式规范,并证明您的程序是正确的.
如果你的目标是100%正确(这通常是汽车/航空航天工业的要求),你将花费很少的时间编程,并有更多的时间证明.
技巧2:用稍微笨拙的语言(例如Ada的某个子集或OCaml的调整版本)编写软件,并在此过程中编写正确性证明.编程和证明在这里齐头并进.Coq中的编程甚至完全等同于它们!(参见Curry-Howard通信)
在这些情况下,您总是会得到一个正确的程序.(一个错误将保证根植于规范中.)你可能会花更多的时间在编程上,但另一方面你在整个过程中证明它是正确的.
请注意,这两种方法都取决于您手头有正式规范的事实(如何判断正确/不正确的行为),以及正式定义的语言语义(您还能如何判断实际行为是什么)你的程序是).
以下是一些正式方法的例子.如果它是"真实世界",取决于你问的是谁:-)
我只知道一种"可证明正确"的网络应用语言:UR.保证"通过编译器"的Ur程序不会:
Dan*_*wak 23
为了回答这个问题,你真的需要通过"可证明"来定义你的意思.正如Ricky指出的那样,任何带有类型系统的语言都是一种内置证明系统的语言,每次编译程序时都会运行.这些证明系统几乎总是令人遗憾地无能为力 - 回答诸如Stringvs之Int类的问题并避免诸如"列表排序？"之类的问题. - 但它们是证据系统,尽管如此.
不幸的是,您的证明目标越复杂,使用可以检查您的证据的系统就越难.当您考虑图灵机上不可判定的类问题的绝对大小时,这会很快升级为不可判定性.当然,理论上你可以做一些基本的事情,例如证明你的排序算法的正确性,但除此之外的任何东西都会在非常薄的冰上踩踏.
即使为了证明像排序算法的正确性这样简单的事情,也需要相对复杂的证明系统.(注意:既然我们已经确定类型系统是一种内置于语言中的证明系统,我将用类型理论来讨论事物,而不是更加努力地挥动我的手)我很确定列表排序的完整正确性证明需要某种形式的依赖类型,否则您无法在类型级别引用相对值.这立即开始进入类型理论领域,这已被证明是不可判定的.因此,虽然您可能能够在列表排序算法上证明正确性,但唯一的方法是使用一个系统,该系统还允许您表达无法验证的证据.亲身,
我之前提到的还有易于使用的方面.您的类型系统越复杂,使用起来越不愉快.这不是一个严格而快速的规则,但我认为它在大多数情况下都适用.和任何正式系统一样,您经常会发现表达证明比首先创建实现更有效(并且更容易出错).
尽管如此,值得注意的是Scala的类型系统(如Haskell的)是Turing Complete,这意味着理论上你可以使用它来证明代码的任何可判定属性,前提是你已经在这样的代码中编写了代码.它适用于这种证据的方式.Haskell几乎肯定是比Java更好的语言(因为Haskell中的类型级编程类似于Prolog,而Scala中的类型级编程更类似于SML).我并不建议您以这种方式使用Scala或Haskell的类型系统(算法正确性的形式证明),但该选项在理论上是可用的.
总而言之,我认为你在"现实世界"中没有看到正式系统的原因在于,形式证明系统已经屈服于实用主义的无情暴政.正如我所提到的,在制作正确性证明方面需要付出很多努力,以至于它几乎不值得.很久以前,业界决定创建临时测试比通过任何分析形式推理过程更容易.
Ric*_*son 10
键入的语言证明没有某些类别的错误.类型系统越先进,它们可以证明缺少的故障越多.
为了证明整个程序是有效的,是的,你走出了普通语言的界限,数学和编程相遇,握手,然后继续使用希腊符号谈论程序员如何处理希腊符号.无论如何,那是关于它的Σ.
Cha*_*tin 10
你问了我们很多人多年来一直在问的问题.我不知道我有一个很好的答案,但这里有一些部分:
有一些易于理解的语言,有可能在今天被证明使用; 通过ACL2的Lisp是一个,当然Scheme也有一个易于理解的正式定义.
许多系统都试图使用纯函数式语言,或几乎纯粹的函数式语言,如Haskell.在Haskell中有一些正式的方法.
回溯20多年,使用正式语言的手工证明是一件短命的事情,然后将其严格翻译成编译语言.一些例子是IBM的软件清洁室,ACL,Gypsy和计算逻辑的Rose,John McHugh和我关于C的可靠编译的工作,以及我自己关于C系统编程的手工证明的工作.这些都得到了一些关注,但没有一个在实践中做得很多.
我认为,一个有趣的问题是,将正式方法付诸实践的充分条件是什么？我很想听听一些建议.
| 归档时间： |
|
| 查看次数： |
7293 次 |
| 最近记录： |