testing - 如何确保所有情况都包含在基于事件的并发设置中？

在SICP 3.4.2 中存在不同进程中事件顺序的问题。

假设我们有两个进程，一个具有三个有序事件 (a,b,c)，一个具有三个有序事件 (x,y,z)。如果两个进程同时运行，并且对它们的执行如何交错没有限制，那么事件有 20 种不同的可能排序，这些排序与两个进程的单独排序一致。

作为设计这个系统的程序员，我们必须考虑这 20 个排序中每一个的影响，并检查每个行为是否可以接受。随着进程和事件数量的增加，这种方法很快变得笨拙。

是否有任何工具/最佳实践可以帮助程序员确保涵盖每个逻辑上不同的情况？

如果程序员可以在它们之间定义一组事件和约束，并且该工具将返回所有有效的事件顺序（识别和分组类似的循环模式），那就太好了。

给定可能的事件流列表，程序员将能够添加/删除/修改约束。

这个问题对我来说很重要，因为我遇到的最多的错误与一些竞争条件或一些未处理的情况有关。

我真的不想使用具有某些高级类型系统的特定语言，我宁愿拥有一种独立于技术/语言的解决方案，它充当某种助手 - 设计和记录系统：及其事件、约束（和状态）。

这对我来说将是圣杯。

我正在寻找这些主题的解决方案：形式方法、形式验证、序言（因为详尽的搜索和逻辑）、并发性、依赖类型、基于事件的编程、多种类型的测试、契约式设计、圈复杂度；但他们都没有给我答案。此外，深入研究类型理论似乎是一种矫枉过正。

标签： testingconcurrencydeveloper-toolsformal-verificationevent-based-programming

“三个有序事件（a，b，c）”
这取决于存在多少交错状态以及需要（在哪个时间）共享哪些资源。查看并发理论的书籍以获取完整的语言理论。不知何故，您需要形式化流程的依赖关系[再次依赖于代码]

竞争条件和未处理的案例可以减少到范围和资源，所以从广义上讲，您要么需要限制表达的可能性，以根据错误案例正式/自动验证您的代码，要么您需要限制资源。

在语言/编程中，这是通过例如模式、良好的 API、语言结构等来完成的。但是没有通用特性，它取决于用例。

竞争条件和未处理的案例看起来您需要更强的打字和自动资源约束，否则您的软件设计可能存在缺陷。