问题标签 [correctness]

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

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

最小生成树问题是采用连通加权图并找到其总权重最低的边的子集，同时保持图连接（并因此产生无环图）。

我正在考虑的算法是：

• 查找所有循环。
• 从每个循环中删除最大的边缘。

这个版本的推动力是一个仅限于“规则满足”的环境，没有任何迭代构造。它也可能适用于疯狂并行的硬件（即，您希望并行度比周期多几倍的系统）。

编辑：

以上以无状态方式完成（在任何循环中不是最大边的所有边都被选中/保留/忽略，所有其他边都被删除）。

多线程算法特别难以设计/调试/证明。Dekker 算法是一个很好的例子，说明了设计一个正确的同步算法是多么困难。Tanenbaum 的现代操作系统在其 IPC 部分中充满了示例。有没有人对此有很好的参考（书籍，文章）？谢谢！

这些for循环是算法形式正确性证明的第一个基本示例。它们具有不同但等效的终止条件：

差异在后置条件中变得很明显：

• i == N第一个给出了循环终止后的有力保证。

• 第二个只给出了循环终止后的弱保证i >= N，但你会很想假设i == N.

如果由于任何原因增量++i更改为类似i += 2，或者如果i在循环内被修改，或者如果N为负数，则程序可能会失败：

• 第一个可能会陷入无限循环。它在有错误的循环中提前失败。调试很容易。

• 第二个循环将终止，并且在稍后的某个时间，由于您对i == N. 它可能会在远离导致错误的循环的地方失败，从而难以追溯。或者它可以默默地继续做一些意想不到的事情，这更糟糕。

您更喜欢哪种终止条件，为什么？还有其他考虑吗？为什么许多知道这一点的程序员拒绝应用它？

使用随机数生成器时，这是使用它来获得新值更大随机性的更好方法：

1. 有一个方法可以每次实例化一个新的 RNG 实例然后返回一个值吗？

2. 在类级别有一个 RNG 实例，它在构造函数中实例化一次，并且所有后续调用都使用现有实例来调用新的随机值？

问题是可能有很多对随机数的调用，通常在不同的范围内，彼此没有联系。

这不是性能问题，因此每个调用都可能实例化一个新实例这一事实没有任何区别。这都是关于返回值的随机性。

我有一个问题，我想学习解决这个问题的正确方法。

我有一个数据对象

我想向用户展示一个使用 LinkHolder.Text 值作为描述性文本的 RadioButton 列表。然后在回发时，我想做一个

在相应的链接上。

我不确定最好/最正确的方法是什么。任何提示将不胜感激。

是否有系统或有开发的带有正确性证明的软件来支持它？还是所有关键系统都只是通过积极的代码审查和测试周期开发的？

我们小组正在构建一个模拟工业过程的过程建模应用程序。这个过程的最终输出是一组代表化学和流速的数字。

该应用程序基于一些非常古老的软件，这些软件使用完全相同的基础数学模型来创建模拟。模拟中涉及数以千计的变量。

尽管每个组件都经过了单元测试，但我们现在需要能够确保我们的软件产生的数据输出与旧模拟软件的输出相匹配。我想知道如何以正式和严格的方式最好地解决这个问题。

旧程序通过文本文件指定输入来工作，所以我想我们可以以编程方式获取每个变量，在文件中调整其值（以及相应地在我们的新应用程序中），然后比较新旧应用程序之间的输出。我们对模型中的每个变量都这样做。

我们知道每个变量的允许范围，所以我认为每个变量的几个值的随机样本足以显示该特定变量的正确性。

对这种方法有什么想法吗？还有其他想法吗？

如果您正在测试如下所示的计数函数，那么在一个函数中为函数测试多个事物与为每个测试都有一个测试函数是“正确的”还是“错误的”？

有什么方法可以强制 Maven 使用远程工件而不是安装在您机器上的那些？因为我担心运行时错误而不是编译错误，所以构建服务器不是有效选项。

PS 我知道我可以删除或重命名 .m2 文件夹，但我敢打赌有一些更聪明的方法可以做到这一点。也许是一些插件或特殊的命令参数？