问题标签 [formal-methods]

我有一个来自 Derek Andrews 和 Darrel INCE 的 VDM 实用形式方法第 5 章的问题，我不确定如何回答，所以在这里，感谢您的帮助！

如果地图价格与汽车价格相关，则集合BL包含 British Leyland 制造的汽车和Fiat 菲亚特制造的汽车。使用本章和集合章节中描述的地图工具和集合工具写下以下描述。

(d) 价格在 6000 英镑到 7000 英镑之间的菲亚特汽车的数量

这是我目前的想法...

1.获取所有法币的价格，即price(fiat)返回价格图的子集

即{punto -→ 5500, panda -→ 6600}

2.可能在地图上限制价格范围（法币）...

但我不确定这是否合法

我认为这应该相对简单，想知道是否有人知道如何回答这个问题：

定义一个递归函数 seq-min : N+ -> N 返回自然数序列中的最小值。

我在想一些类似的事情......

谢谢你的帮助！

使用最新（不稳定）Z3运行z3 -p会显示按模块分组的参数列表。说明如下：

一般来说，这些指令如何转换为 C API？在当前文档中，似乎有一组 API 调用处理“全局”配置，例如 ，Z3_set_param_value以及围绕该Z3_params类型构建的另一组特定于对象的调用，例如Z3_solver_set_params.

特别是，我想知道是否可以使用Z3_set_param_value全局设置任何模块中的任何参数。其他 StackOverflow 答案甚至宣传Z3_params对象的使用，即使是全局参数，比如timeout（或者是:timeout？），但我不清楚这个 API 如何映射到module.parameter=value语法。

看看 C，C 对可以在代码中使用的形式化方法有很好的支持（frama-c、VCC、verifast）。据我所知，C++ 似乎没有任何可比性。

有哪些形式化方法可用于推理用 C++ 编写的安全关键软件？

我正在阅读这本书：1990 年代的编程。

我在解决要求我们解决的练习 10.12 时遇到困难：

我引入了新的变量 n 使得

这导致我不变

和守卫

绑定函数是

任务取得进展

我知道解决方案很简单，但是在尝试保持 I0 的不变性时总是卡住。

请有人告诉我如何计算分配以保持 I0 的不变性？

谢谢。

是否有正式/传统的方式来描述数据/命令交换协议？例如，对于编程语言，有多种方法来描述语法和语义（例如：http ://en.wikipedia.org/wiki/Backus%E2%80%93Naur_Form ）。

我正在寻找的方法是相当实用的（与学术相反）。在制定规范时，我需要一些用于日常数据交换描述的东西，只是为了将这个想法清楚地传递/传播给其他人。所以，如果有一些东西不被认为是事实上的标准但很有用——那也没关系。

我查看了 UML 序列图和“通信协议规范和验证的形式化方法，Carl A. Sunshine，1979 年”。前一种方法缺少对“有效负载”的描述（至少从我的理解来看），而后一种方法更像是一篇描述考虑因素而不是方法的教育性论文（不过，我仍在阅读这篇论文）。

提前致谢

给定一个循环不变量，维基百科列出了一个为循环生成最弱前提条件的好方法（来自http://en.wikipedia.org/wiki/Predicate_transformer_semantics）：

M[x <- N] 用 N 替换 M 中所有出现的 x。

现在，我的问题是变量 y。\forall y, 在表达式中绑定 y，因此“y 是新变量的元组”不会为我解析。\forall 中的 y 是否与 "[x <- y]" 中的 y 相同？我根本无法解析上述内容。

编辑：改写以避免参考请求。

我的问题是：循环不变量和计算最弱前提（如果有的话）之间的直接联系是什么。似乎在实践中所做的很多事情都将循环的最弱前提条件放松为适合验证的前提条件。来自维基百科的上述内容表明，给定一个循环不变量，确实可以计算出鼻子上最弱的先决条件，但我无法理解这个条件。

示例 1

示例 2

这些句子中的 <> 是什么意思？

我一直在阅读有关 SonarQube 源代码分析平台的信息，我一直在想：形式方法呢？

我看到PMD和FindBugs等工具可以轻松集成，因为它的架构促进了插件的使用。然而，我没有看到基于抽象解释的分析器，甚至没有任何提到基于形式方法的工具。

我想知道这是否与基于规则的集成插件方法的限制有关？

我读到他们正在改进 Java 的语义分析，也许这可以启用基于正式方法的方法......

有人有更多的信息吗？比如，SonarQube 团队是否有兴趣朝着这个方向发展？

谢谢！

我发现的所有示例都只有 2 个声明such as name and date OR members and telephone。但是，我的情况是这样的：

我想创建一个名为 AppointmentDB 的 Z 模式。AppointmentDB 保留约会的详细信息，例如目的、参加者和日程安排

我的看法（已编辑）：

有 5 个声明和 1 个谓词

如您所见，我正在尝试将 APPOINTMENT 链接到它的所有其他属性。我的架构是否正确或完整，或者如何进一步优化它？另外，我怎么知道我应该从关系中考虑哪个关系来定义谓词部分？