问题标签 [formal-methods]

• 您将模型检查用于哪些类型的应用程序？
• 你用的是什么模型检查工具？
• 您如何总结您使用该技术的经验，特别是在评估其交付更高质量软件的有效性方面？

在我的学习过程中，我有机会使用Spin，它引起了我的好奇心，即实际进行了多少模型检查以及组织从中获得了多少价值。在我的工作经验中，我从事过业务应用程序，其中（自然）没有考虑将形式验证应用于逻辑。我真的很想了解 SO 人的模型检查经验和对该主题的想法。模型检查会成为我们应该在我们的工具包中使用的更广泛使用的开发实践吗？

所以...

我在软件工程中教授形式化方法。我还教授“敏捷方法”。大多数人似乎认为这是矛盾的。我认为这很有意义......我也在一家公司工作，我们需要真正完成工作:) 虽然我可以将我获得的技能点应用于日常的“规范”，但我的同事们通常会避开“正式”这个词。

我曾经认为这是由于我们学习编程的内在方式：我们通常被驱使寻找可行的解决方案，而不是理解问题。然后我认为这是因为正式社区中的大多数人不是工程师，而是数学家或计算机科学家。如今，我想知道是否只是因为形式方法社区隐藏在某种“混淆”法律的背后，才使用所有可用的 UNICODE 符号，积极开发粗鲁、不美观的工具，并在标准面前大笑。

是的，我一直在从“责备他们”转变为“责备我们”的观点；-)

所以，我的问题是：您在公司中使用任何形式的方法吗？你有没有介绍过它们，或者它们是先决条件？你使用什么技术来消除人们恐惧中的数学迷雾并鼓励他们使用形式化方法？您认为当前的工具缺少哪些更通用的用途？

我们的客户希望我们构建一个基于 Web 的富 Internet 应用程序来收集软件需求。基本上，它是一个基于 Web 的案例工具，遵循特定流程从利益相关者那里获取需求。我是项目经理，我们仍处于项目的早期阶段。

我一直在考虑使用形式化方法来帮助我的客户和开发人员澄清对工具的要求。我所说的形式方法是指某种形式的建模，可能是基于数学的。我已经阅读并正在考虑的一些内容包括 Z ( http://en.wikipedia.org/wiki/Z_notation )、状态机、UML 2.0（可能带有OCL等扩展）、Petri 网和一些编码合同和前置条件和后置条件等级别的东西。还有什么我应该考虑的吗？

开发人员经验丰富，但根据所使用的形式，他们可能需要学习一些数学知识。

我正在尝试确定我是否值得在这个项目上使用形式化方法，如果是，在多大程度上。我知道“这取决于”，所以对我来说最有帮助的答案是是/否和支持论点。

如果你在这个项目中，你会使用正式的方法吗？

这是一个奇怪的问题。我正在写一本关于学习使用正式方法进行编程的书，并且我将把它针对具有一些编程经验的人。这个想法是教他们成为高质量的程序员。

基本符号将来自 Dijkstra 的Discipline of Programming，以及一些并发和通信扩展。

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

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

我是一名对信息检索感兴趣的软件开发人员。目前我正在处理我的第三个搜索引擎项目，并且对一次又一次编写的样板代码数量感到非常沮丧，同样的错误等等。

基本搜索引擎是一个非常简单的野兽，可以用由两个“层”组成的正式语言来描述：

1. “原语层”（或公理，内核语言 - 不知道如何命名它们）。它们包括几个集合（作为一组资源 - 文件、网站）、集合上的关系（作为“站点 A 链接到站点 B”）和简单的操作，例如“打开资源 A 的流”、“从流中读取记录”、 'merge N 个流'，'index set of records by field F'等。还有很多数据转换，如'save stream in YAML format'，'load stream from XML format'等。

2. “应用层”——构成搜索引擎生命周期的几个非常高级的操作，如“收获新资源”、“抓取收获的资源”、“将抓取的资源合并到数据库”、“索引抓取的资源”、“合并索引”等等。每一个高级操作都可以用从 1 开始的“原语”来表示。

这种高级表示可以很容易地测试，甚至可以正式证明，并用所选的编程语言实现（或代码生成）。

那么问题来了：是否有人以这种方式设计系统——形式上、严格（甚至可能在代数/群论的层面上），在严格的自上而下的方法中？我可以阅读以了解什么？

一段时间以来，我一直对形式化方法感兴趣。我已经使用正式的方法来推理我一直在从事的几个项目的一些非常具体的子领域。我永远无法说服其他团队成员尝试相同的方法，更不用说使用正式的方法指定整个域了。

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

我很想听听你们在项目中使用 Alloy 的实际经验。你觉得它帮助你设计了一个更好的领域模型吗？验证期间是否在您的域模型中发现错误？你会再次使用它吗？

我希望能够将大测试拆分为较小的测试，以便当较小的测试通过时，它们暗示大测试也会通过（因此没有理由运行原始的大测试）。我想这样做是因为较小的测试通常需要更少的时间、更少的精力并且更不脆弱。我想知道是否有测试设计模式或验证工具可以帮助我以稳健的方式实现这种测试拆分。

我担心当有人更改较小测试集中的某些内容时，较小测试和原始测试之间的联系会丢失。另一个担心是较小的测试集并没有真正涵盖大的测试。

我的目标是一个例子：

我正在检查软件的模型一致性。为此，我需要为 UML 2.0 序列图编写线性时序逻辑。如果任何机构有任何其他相同的工具，请尽快回复。我会很感激你的。我发现迷人的工具有相同的插件。有没有人有魅力工具的源代码（检查建筑模型一致性）。它在他们的网站上不可用。

提前致谢。

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

我在编程生涯中比较晚才接触到Curry-Howard 同构，也许这有助于我对它完全着迷。这意味着对于每个编程概念，在形式逻辑中都存在一个精确的类比，反之亦然。这是我想不到的此类类比的“基本”列表：

那么，对于我的问题：这种同构有哪些更有趣/更晦涩的含义？我不是逻辑学家，所以我确信我只是用这个列表触及了表面。

例如，以下是一些我不知道逻辑中精辟名称的编程概念：

以下是一些我在编程术语中尚未完全确定的逻辑概念：

编辑：

以下是从回复中收集的更多等价物：