我在大学时瞥见了Hoare Logic。我们所做的非常简单。我所做的大部分工作是证明由while循环、if语句和指令序列组成的简单程序的正确性，但仅此而已。这些方法看起来很有用！
形式化方法是否在工业中广泛使用？
这些方法是否用于证明关键任务软件？
问问题
1779 次
10 回答
14
好吧，Tony Hoare 爵士大约在 10 年前加入了微软研究院，他开始的一件事就是对 Windows NT 内核进行形式化验证。确实，这也是 Windows Vista 迟迟不来的原因之一：从 Vista 开始，内核的大部分实际上都是经过正式验证的 wrt。对于某些属性，例如没有死锁，没有信息泄漏等。
这当然不是典型的，但就其影响而言，它可能是形式程序验证中最重要的一个应用（毕竟，几乎每个人都在某种程度上受到运行 Windows 的计算机的影响）。
于 2009-07-28T21:32:49.023 回答
12
这是一个贴近我心的问题（我是使用形式逻辑进行软件验证的研究员），所以当我说我认为这些技术有一个有用的地方，并且在行业。
有许多级别的“形式方法”，所以我假设你的意思是那些基于严格的数学基础的（而不是，比如说，遵循一些 6-Sigma 风格的过程）。某些类型的形式化方法取得了巨大的成功——类型系统就是一个例子。基于数据流分析的静态分析工具也很流行，模型检查在硬件设计中几乎无处不在，像 Pi-Calculus 和 CCS 这样的计算模型似乎正在激发实际并发语言设计的一些真正变化。终止分析是最近有很多媒体报道的一个——微软的 SDV 项目和 Byron Cook 的工作是形式方法中研究/实践交叉的最新例子。
到目前为止，Hoare Reasoning 还没有在该行业取得重大进展 - 这比我能列出的原因更多，但我怀疑主要是围绕编写和证明真实程序规范的复杂性（它们往往会变大，然后失败）来表达许多现实世界环境的属性）。这类推理的各个子领域现在正在大举解决这些问题——分离逻辑就是其中之一。
这部分是正在进行的（硬）研究的性质。但我必须承认，作为理论家，我们完全未能教育行业了解我们的技术为何有用，无法让它们与行业需求相关联，并让软件开发人员易于使用。在某种程度上，这不是我们的问题——我们是研究人员，通常是数学家，实际使用并不是我们的首要考虑。此外，正在开发的技术通常还处于萌芽状态，无法用于大规模系统——我们致力于小程序、简化系统、数学运算，然后继续前进。不过，我不太相信这些借口——我们应该更积极地推动我们的想法，并在行业和我们的工作之间建立一个反馈循环（我重新研究的主要原因之一）。
恢复我的博客对我来说可能是个好主意，并在这些东西上发表更多帖子......
于 2009-07-28T22:02:52.907 回答
6
我不能对关键任务软件发表太多评论，尽管我知道航空电子行业使用多种技术来验证软件，包括 Hoare 式方法。
正式方法受到了影响，因为像 Edsger Dijkstra 这样的早期倡导者坚持认为它们应该在任何地方使用。形式主义和软件支持都不能胜任这项工作。更明智的倡导者认为，这些方法应该用于解决困难的问题。它们在工业中并未广泛使用，但采用率正在增加。可能最大的进展是使用正式的方法来检查软件的安全属性。我最喜欢的一些例子是SPIN模型检查器和 George Necula 的证明携带代码。
从实践转向研究，微软的Singularity操作系统项目是关于使用正式的方法来提供通常需要硬件支持的安全保证。这反过来又会带来更快的性能和更强的保证。例如，他们已经证明，如果允许第三方设备驱动程序进入系统（这意味着已经证明了基本验证条件），那么它不可能破坏整个操作系统——最糟糕的是它可以做的就是管它自己的设备。
形式化的方法在工业上还没有广泛使用，但比 20 年前更广泛地使用，20 年后它们将更广泛地使用。所以你是面向未来的:-)
于 2009-07-28T23:47:47.907 回答
5
是的，它们被使用，但并非在所有领域都广泛使用。有更多的方法，而不仅仅是简单的逻辑，有些使用得更多，有些使用得更少，这取决于对给定任务的适用性。常见的问题是软件是 biiiiiiig 并且验证所有这些都是正确的仍然是一个太难的问题。
例如，定理证明器（一种帮助人类证明程序正确性的软件）ACL2 已被用于证明某个浮点处理单元不存在某种类型的错误。这是一项艰巨的任务，因此这种技术并不太常见。
模型检查是另一种形式化验证，现在应用比较广泛，例如微软在驱动程序开发包中提供了一种模型检查器，它可以用来验证驱动程序的一组常见错误。模型检查器也经常用于验证硬件电路。
严格的测试也可以被认为是形式验证——有一些形式规范应该测试哪些程序路径等等。
于 2009-07-28T21:33:08.647 回答
3
“工业中使用形式化方法吗？”
是的。
许多编程语言中的assert语句与验证程序的形式化方法有关。
“形式化方法在工业中广泛使用吗？”
不。
“这些方法是否用于证明关键任务软件？”
有时。更多时候，它们被用来证明软件是安全的。更正式地说，它们用于证明有关软件的某些与安全相关的断言。
于 2009-07-28T21:24:37.650 回答
2
业界有两种不同的形式化方法。
一种方法是完全改变开发过程。提到的 Z 表示法和 B 方法属于第一类。B被应用于巴黎14号线无人驾驶地铁的开发（如果有机会，爬上前车厢。很少有机会看到前面的铁轨）。
另一种更渐进的方法是保留现有的开发和验证过程，并一次只用一种新方法替换一个验证任务。这是非常有吸引力的，但这意味着开发静态分析工具以用于现有的、使用的语言，这些语言通常不容易分析（因为它们不是设计成的）。如果你去（例如）
http://dblp.uni-trier.de/db/indices/a-tree/d/Delmas:David.html
（对不起，新用户只允许一个超链接：（）
您将找到形式化方法在验证 C 程序（使用静态分析器 Astrée、Caveat、Fluctuat、Frama-C）和二进制代码（使用 AbsInt GmbH 的工具）中的实际应用实例。
顺便说一句，既然您提到了Hoare Logic，那么在上面的工具列表中，只有Caveat 是基于Hoare 逻辑的（并且Frama-C 有一个Hoare 逻辑插件）。其他人则依赖于抽象解释，这是一种具有更自动化方法的不同技术。
于 2009-08-03T22:08:48.197 回答
2
我的专业领域是使用形式化方法进行静态代码分析，以表明软件没有运行时错误。这是使用称为“抽象解释”的形式方法技术实现的。该技术本质上使您能够证明 as/w 程序的某些属性。例如，证明 a+b 不会溢出或 x/(xy) 不会导致除以零。使用这种技术的一个示例静态分析工具是 Polyspace。
关于您的问题：“形式方法是否广泛用于工业？” 和“这些方法是否用于证明关键任务软件？”
答案是肯定的。此观点基于我的经验，并支持 Polyspace 工具适用于依赖使用嵌入式软件来控制安全关键系统的行业，例如汽车电子节气门、火车制动系统、喷气发动机控制器、药物输送输液泵、等等。这些行业确实使用这些类型的形式化方法工具。
我不相信所有这些行业领域都 100% 都在使用这些工具，但使用量正在增加。我的观点是，航空航天和汽车行业引领着医疗器械行业的快速普及。
于 2011-08-19T18:08:57.780 回答
1
Polyspace是一个基于程序验证的商业产品（非常昂贵，但非常好）。这是相当实用的，因为它从“可能会发现一些错误的增强单元测试”扩展到“你将在接下来的三年中花费时间来证明这 10 个文件的缺陷为零”。
它更多地基于否定验证（'这个程序不会破坏你的堆栈'）而不是肯定验证（'这个程序将完全按照这 50 页方程所说的那样做'）。
于 2009-07-28T22:52:14.197 回答
0
除了其他更程序化的方法之外，Hoare 逻辑是基于契约设计的，由 Bertrand Meyer 在 Eiffel 引入的一种面向对象的技术（参见 Meyer 的 1992 年文章，第 4 页）。虽然按合同设计与形式验证方法不同（一方面，DbC在软件执行之前不会证明任何东西），但在我看来，它提供了更实际的用途。
于 2009-10-27T10:44:16.163 回答