标签: formal-methods

我在编程生涯中相对较晚地遇到了Curry-Howard Isomorphism,也许这有助于我对它完全着迷.这意味着对于每个编程概念,在形式逻辑中存在精确的模拟,反之亦然.这是一个关于这种类比的"基本"列表,在我的头脑中:

program/definition        | proof
type/declaration          | proposition
inhabited type            | theorem/lemma
function                  | implication
function argument         | hypothesis/antecedent
function result           | conclusion/consequent
function application      | modus ponens
recursion                 | induction
identity function         | tautology
non-terminating function  | absurdity/contradiction
tuple                     | conjunction (and)
disjoint union            | disjunction (or)          -- corrected by Antal S-Z
parametric polymorphism   | universal quantification

那么,对于我的问题:这种同构的一些更有趣/模糊的含义是什么？我不是逻辑学家,所以我确信我只是在这个清单上划过界限.

例如,这里有一些编程概念,我不知道逻辑中精辟的名字:

currying                  | "((a & b) => c) iff (a => (b => c))"
scope                     | "known …

继续观念:有没有可证明的现实世界语言？

我不了解你,但我厌倦了编写我无法保证的代码.

在询问了上述问题并得到了非凡的回应之后(谢谢大家!)我决定缩小我对Haskell的可证明,实用的方法的搜索范围.我选择哈斯克尔,因为它是真正有用的(也有许多 网页 框架为它写在纸上,这似乎是一个很好的基准)和我认为这是不够严格,在功能上,它可证明的,或者至少允许不变量的测试.

这就是我想要的(并且一直无法找到)

我想要一个可以查看Haskell函数的框架,添加,用psudocode编写:

add(a, b):
    return a + b

- 并检查某些常量是否保持每个执行状态.我更喜欢一些正式的证据,但是我会满足于像模特检查员这样的东西.
在此示例中,不变量将是给定值a和b,返回值始终是总和a + b.

这是一个简单的例子,但我不认为这样的框架不可能存在.对于可以测试的函数的复杂性肯定会有一个上限(函数的10个字符串输入肯定会花费很长时间!)但这会鼓励更仔细地设计函数,并且与使用其他正式函数没有什么不同方法.想象一下,使用Z或B,当您定义变量/集时,您可以确保为变量提供尽可能小的范围.如果您的INT永远不会超过100,请确保将其初始化为!像这样的技术和正确的问题分解应该 - 我认为 - 允许对像Haskell这样的纯函数语言进行令人满意的检查.

我还没有 - 使用正式方法或Haskell非常有经验.让我知道我的想法是否合理,或者你认为haskell不合适？如果您建议使用其他语言,请确保通过"has-a-web-framework"测试,并阅读原始问题 :-)

与Coq相比,Isabelle/HOL证明助手是否有任何弱点和优势？

看看C,C对可以在代码中使用的形式方法(frama-c,VCC,verifast)有很好的支持.就我所知,C++似乎没有任何可比性.

有哪些正式方法可用于推理用C++编写的安全关键软件？

这是一个奇怪的问题.我正在编写一本关于学习使用正式方法编程的书,我将把它定位到具有一些编程经验的人.我们的想法是让他们成为高素质的程序员.

基本符号将来自Dijkstra的编程规则,以及一些并发和通信扩展.

与EWD不同,我希望我的学生最终能够编写实际的可执行程序.这意味着在某些时候从EWD符号转换为其他语言.当我第一次开始正式编程时,我以C为目标,但你最终编写了大量的管道,加上处理指针的所有复杂性等.Ruby是一个明显可能的目标,如Scheme或Lisp.但也有各种函数语言; 因为我对并发特别感兴趣,所以Erlang似乎是一种可能性.

所以,最后,我的问题是:我应该用什么语言教我的读者定位他们正式开发的程序？

传统上大多数使用计算逻辑的工作要么是命题,在这种情况下你使用了SAT(布尔可满足性)求解器,或者是一阶,在这种情况下你使用了一阶定理证明器.

近年来,SMT(可满足模理论)求解器取得了很大进展,基本上用算术等理论来增强命题逻辑.SRI International的John Rushby甚至称他们为颠覆性技术.

在一阶逻辑中可以处理但仍然无法由SMT处理的问题最重要的实际例子是什么？最特别的是,SMT在软件验证领域无法解决哪些问题？

一段时间以来,我一直对正式方法感兴趣.我使用了正式的方法来推理我一直在研究的一些项目的一些非常具体的子领域.我永远无法说服其他团队成员尝试同样的,更不用说用正式方法指定整个域了.

我发现一种特别有趣的方法是Alloy.我认为它可以作为整个项目的基础更好地"扩展",因为它在概念上和符号上非常接近实际的编程语言.此外,这些工具非常可靠,因此可以轻松获得模型验证的好处.

我非常有兴趣了解您在项目中使用Alloy时可能遇到的任何实际经验.您是否认为它帮助您设计了更好的域模型？在验证期间是否在您的域模型中发现错误？你会再次使用它吗？

当使用形式方面来创建一些代码时,是否有一种确定循环不变量的通用方法,或者它是否会根据问题完全不同？

我试图(经典地)证明

~ (forall t : U, phi) -> exists t: U, ~phi

在Coq.我想要做的是证明它是相反的:

1. Assume there is no such t (so ~(exists t: U, ~phi))

2. Choose arbitrary t0:U

3. If ~phi[t/t0], then contradiction with (1)

4. Therefore, phi[t/t0]

5. Conclude (forall t:U, phi)

我的问题是第(2)和(5)行.我无法弄清楚如何选择U的任意元素,证明它的一些东西,并得出一个结论.

任何建议(我不承诺使用对立面)？

所以...

我教授软件工程中的正式方法.我还教授"敏捷方法论".大多数人似乎认为这是矛盾的.我认为这很有意义......我也在一家公司工作,我们需要在那里完成任务:)虽然我可以在日常的基础上应用我所获得的技能点"我的规格",同事们通常会逃避"正式"这个词.

我曾经认为这是由于我们学习如何编程的内在方式:我们通常会找到一个有效的解决方案而不是理解问题.然后我认为这是因为正式社区中的大多数人不是工程师,而是数学家或计算机科学家.如今,我想知道是否只是因为正式方法社区隐藏在某种"混淆"法律背后,使用所有可用的UNICODE符号,积极开发粗鲁,不实用的工具,并在标准面前笑.

是的,我一直在从"责备他们"转变为"责备我们"的观点;-)

所以,我的问题是:你在公司使用任何形式的方法吗？你介绍过它们,还是它们的先决条件？你用什么技巧来消除人们的恐惧中的数学迷雾,并煽动他们使用正式的方法？您认为目前的工具缺乏更普遍的用途？