问题标签 [formal-methods]

我在 ALLOY 中有一段代码我正在尝试做一个餐厅预订系统，我有这个信号和它们之间的关系。

我想说明一个事实，早餐可以预订或免费，午餐和晚餐都一样，有什么想法吗？

我正在进行一些研究，并没有找到太多的文献来帮助，我想比较两种形式化方法的平台依赖关系；代数规范和面向对象。他们会使用哪种语言？

有没有人对此有任何了解或可以指出我正确的方向？谢谢

我希望有人可以帮助我解决以下问题，答案将是最好的，但如果你能指出我正确的方向，那也会有所帮助。我是大学最后一年的学生，这些问题来自之前的形式方法考试，我可以知道为今年论文准备的答案。我们的讲师似乎不是最好的，并且没有涵盖很多内容，因此事实证明不可能找到确切的答案。谷歌并没有太大的帮助，也没有推荐的书籍。

1 - 假设 ∃x • P (x) 在逻辑上等价于 ¬∀x • ¬P (x) 并且 ∀x ∈ S • P (x) 意味着 ∀x • x ∈ S ⇒ P (x)，推导出∃x ∈ S • P (x) 表示 ∃x • x ∈ S ∧ P (x)

2 - 描述必须证明的两个陈述以表明定义：

是规范的正确实现：

我想知道是否有人可以帮助我回答这个问题。它来自以前的试卷，我可以知道为今年考试准备的答案。

这个问题似乎很简单，以至于我完全迷失了，它到底在问什么？

考虑以下涉及整数变量的代码部分：

通过陈述一个合适的输出条件，然后验证这段代码的正确性，证明执行后m等于i和j的最小值。

我的后置条件为：{m = i ∧ i < j ∨ m = j ∧ j < i}

它是否正确？你如何验证这一点？

我是一名（理论）计算机科学专业的学生，​​因此研究编程语言的语义是我研究的主题之一（维基百科）。

我玩过很多 CSS 并且对盒子的定位规则有一个合理的理解。（如果你告诉我创建一个具有特定布局的页面，我通常可以想到正确的框方法和适用的 CSS 规则。）

为 CSS 框定位规则提供某种形式的语义会很酷，但是在网上搜索了一段时间后，我找不到任何有用的东西。

我大多只是简单地以 CSS 规范结束，这些规范被格式化为带有伪算法的长文本（不是最好的阅读材料——我还没有花太多精力阅读这些规范中的任何一个）。

没有人试图将这个“理论”形式化为某种数学模型，比规范所提供的更严格吗？我不是在寻找完整或确定的东西，但如果至少可以以正式的方式对盒子的放置方式进行建模，那么它肯定会很整洁（而且很有用！）。

有人知道这样的研究吗？

Traditionally most work with computational logic was either propositional, in which case you used a SAT (boolean satisfiability) solver, or first-order, in which case you used a first-order theorem prover.

In recent years, a lot of progress has been made on SMT (satisfiability modulo theory) solvers, which basically augment propositional logic with theories of arithmetic etc.; John Rushby of SRI International goes so far as to call them a disruptive technology.

What are the most important practical examples of problems that can be handled in first-order logic but still can't be handled by SMT? Most particularly, what sort of problems arise that can't be handled by SMT in the domain of software verification?

根据 Alloy 4.2 的发行说明，存在与整数相关的语义更改。这些变化似乎对 Alloy 书的练习 A.1.6 产生了影响。

在本练习中，以以下代码为基础（我在最后添加了“Int”以显示我的问题）。当运行“show”谓词时，可视化器显示一个实例，但这个实例除了整数之外还包含两个原子“Univ0”和“Univ1”。

这两个原子“Univ0”和“Univ1”是什么意思？他们为什么在那里？它们与在 Alloy 4.1.10 上执行的代码不同。

我是 Z 表示法的完整初学者。我需要在 Z 中表示一个图类型。我的想法是使用关联矩阵，以便我可以轻松地在节点和边之间自由遍历。

唯一的问题是，我不知道如何在 Z 中指定关联矩阵。我认为我需要一个 2D 数组，但是通过可用于 Z 表示法的参考资料，数组通常使用 seq 表示。还有另一种方法来指定多维数组吗？

提前致谢。

假设我有这样的功能：

这个微不足道的函数总是返回 1。使用带有 -O2 选项的 clang 编译并查看反汇编代码 LLVM 正确将此函数编译为return 1;.

我的问题是：llvm如何做静态值分析？最弱的前置条件技术？价值传播？霍尔的技术？

从这个问题跟进...

我有一个完全连通的图，这很棒。我也加入了时间的概念。我现在正在为围绕我的图表传递数据的概念而苦苦挣扎。

我正在为一个系统建模，该系统的任务是确保每个节点都有一个已插入系统的数据副本。我脑子里有关于如何做到这一点的程序，但是我正在努力将其翻译成合金术语。

一个典型的算法看起来像这样：

为简单起见，假设每个节点都有一个唯一的数据，它们必须将该数据提供给所有其他节点。由于这是完全连接的，它应该相对简单（翻译成合金/形式逻辑对我来说有点困难）。

这是我目前所在的位置：

从我的运行谓词中，您可以看到我希望在 20 个时间步内发送所有消息，因此到那时每个 DataMirror 都应该有一组由 5 个唯一消息组成的数据。

我很确定我想做的是让每个 DataMirror 有 2 个属性：

• 要发送的唯一消息（此时可以只是一个简单的变量）
• 收到的消息集（包括原始消息）

当所有 DataMirror 具有相同的消息集时，系统会感到满意。

例如，如果我们有：

那么系统将在以下情况下完成：

我为让任何形式逻辑的高级用户畏缩而提前道歉......我正试图在试炼中学习这一点:)。