问题标签 [formal-methods]

这是我的约会数据库的 Z 模式。

我想创建一个搜索功能，根据attendees.

1. 我希望搜索功能返回约会对象的所有详细信息。

我该如何设计它？

这是我的看法：

Isabelle/HOL 校对助手和 Coq 相比有什么弱点和强项吗？

我有以下身份，它（隐式）定义了正整数的分区数（即，您可以将整数写为有序非零正整数之和的方式数）：

一些注意事项：

1. 这在 Flajolet 和 Sedjewick 的 Analytic Combinatorics 一书中进行了研究，公式的图像取自那里，因为 stackoverflow 不支持 LaTeX。

2. sigma 是一个数的除数之和

我想编写一个计算带有 P 系数的列表的 haskell 程序。第 i 项取决于所有先前的项（是压缩 sigma 和先前 Ps 产生的列表的总和）。这个问题是一个很好的例子，说明如何根据规范“计算”程序，就像 Gibbons 在他的论文中所写的那样。

问题是：是否有已知的递归方案可以捕获这种计算？列表中的每个术语都依赖于所有先前术语的计算，（并且结果与先前的术语无关，我的意思是，您必须对每个术语进行新的遍历）

我是形式方法领域的新手，但我觉得我对它的应用有一定的了解。但是，我似乎只遇到了应用于开发过程的正式方法，因为软件是创建的。

我希望能够在现有软件上应用形式化方法来测试它是否遵循基于角色的访问控制 (RBAC) 和遵循Bell-LaPadula (BLP) 方法的敏感信息分离。

您知道哪些方法和工具可以为现有软件/源代码的 RBAC 和 BLP 类验证提供自动化解决方案？

干杯，

M·福兹

我在 ispin 中建模了一个系统，当尝试使用 LTL 公式验证系统时，我发现了无法访问的错误，例如

我的 ltl 公式是

如果我有一个 8 个地方和 8 个事务的 Petri 网模型。这个模型中没有任何死状态，因为令牌处于循环中并且在第一个循环中经过所有 8 个地方。在第二个和剩余的循环中，它将经过 6 个位置，因为执行 T5 时令牌将到达 Place3。在这里，我想知道可达状态的数量。可达状态是无限的（因为循环）还是什么？

我正在阅读实用逻辑和自动推理手册。它有一些代码来定义文件中的有限部分函数 lib.ml。我无法理解部分函数中重新定义和组合的代码的含义。子功能的目的是什么newbranch？代码如下：

你能为我解释一下这段代码的含义吗？

假设我们有一个列表：

请注意，我说的是可修改列表！还有一个简单的递归长度函数：

自然，它仅在列表非循环时终止：

请注意，这个谓词被实现为递归函数，也不会在循环列表上终止。

通常我会看到使用列表长度作为有界递减因子的列表遍历终止证明。他们认为这Length是非负的。但是，在我看来，这个事实 ( Length l >= 0) 首先是从 of 的终止而来的Length。

你如何证明，在（或等效的，更好定义的谓词）列表Length上终止并且是非负的？NonCircular

我在这里错过了一个重要的概念吗？

进程 a 或进程 b 进入临界区，但不是同时。如果发生这种情况（即它们同时进入临界区），将执行中断。

p = 进程 a

q = 进程 b

r = 临界区

运算符 ∨ = 或

运算符 → = 蕴涵

我的答案 ：

(p ∨ q) → r

这是正确的还是我做错了什么？我试图理解命题逻辑。

我是 Z 表示法的新手，

假设我有一个函数 f 定义为 X |--> Y ，其中 X 是字符串，Y 是数字。

如何在此函数中获得最高 Y 值？形式方法中是否存在“循环”，所以我可以使用循环来解决它？

我知道 Z 表示法中有递归，但根据提供的材料，我发现它只适用于 multiset 或 bag，它可以适用于函数吗？

“循环”或递归应用程序的任何额外参考应用程序将不胜感激。对不起我的英语不好。