问题标签 [formal-semantics]

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

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

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

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

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

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

p = 进程 a

q = 进程 b

r = 临界区

运算符 ∨ = 或

运算符 → = 蕴涵

我的答案 ：

(p ∨ q) → r

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

对于语法，有EBNF ISO 14977 标准。

对于运行时，我们有CLI ISO 23271 标准 ，
另见“语义”的简单定义，因为它通常与编程语言/API 相关？

但是如何以声明的方式描述从 EBNF 到 CLI 规范的过渡？即使用S 属性语法是否足够？哪个标准定义了这种语法的语法？

我一直在阅读有关形式验证的内容，基本观点是它需要一个正式的规范和模型才能使用。然而，许多来源将静态分析归类为一种形式验证技术，一些提到抽象解释并提到它在编译器中的使用。所以我很困惑——如果没有模型的正式描述，这些怎么可能是形式验证？
编辑：我发现的一个来源是：

静态分析：抽象语义是根据预定义的抽象从程序文本中自动计算出来的（有时可以由用户自动/手动定制）

那么这是否意味着它只适用于源代码而无需正式规范？这就是静态分析器所做的。

另外，如果没有形式验证，是否可以进行静态分析？例如，SonarQube 真的执行形式化方法吗？

我定义了 2 种几乎相同的语言（foo 和 bar）：

一个微不足道的语义：

打字：

我还定义了一个从 foo 到 bar 的翻译器：

我试图证明翻译器将 foo 表达式转换为具有相似类型的 bar 表达式：

并且转换还保留了表达式的语义：

我什至证明了一些归纳案例。但我无法证明FooToBar (FooVar x)案例的引理。

一般来说，不能证明 与FooVar x具有相似的类型或值BarVar x。

我想这FooToBar一定更复杂。它还必须涉及某种表达式环境或变量映射。你能推荐一个更好的签名FooToBar吗？我认为这样的翻译器是一件小事，但我找不到任何描述它的教科书。

在 Dafny 上， alemma被实现为 a ghost method，因此，它仅对规范有用。

但是，您不能从 a 调用引理ghost field，如下所示：

这种行为的理由是什么？如何解决？在内部类中重复引理并利用（通常是调用）其他类的最佳选择是lemma什么？

我正在使用K 语义框架并运行教程，这是我的 TEST1.k ：

但是在运行命令 Komile Test1.k 时出现此错误：

从O'Reilly NLTK 书的第 10 章中可以看出，当我想对句子“Bob love Alice”的句法树进行建模时，即

进入一阶逻辑 lambda 表达式，我得到以下信息：

左边是类型树，右边是 λ 表达式树。我选择对 Bob 和 Alice 进行类型加注。

我的问题如下：从类型树中，我可以很容易地计算出“爱”的类型必须是<<<e,t>,t>,<e,t>>，但是我如何从中推断出相应的 λ 表达式必须是

λR.λx.R(λy.loves(x,y))

是否有某种方法可以从语法树的类型和周围的 λ 表达式中获取其叶子的 λ 表达式？

如图，这是一个代码示例，定义了模型转换中源模型和目标模型的数据类型和有趣的功能。前三张图分别对应源模型架构、目标模型架构，以及它们之间的转换关系。最后三张图的递归函数的含义：

图4中定义的函数Part1是基于几个递归函数（如getPlaces等）

图 5 中定义的函数 Part2 基于几个递归函数。（如getTranStep2等）

图6是上面的基本递归函数getPlaces，描述了接收源模型SMD中Allstate列表的参数（包括最终状态、简单状态、复合状态），并返回places，但不考虑SMD初始状态。

最后三张图中递归函数的表达式看不懂，尤其是链接表达式的字符（'''''、[]、@、#、LL、st、substs），让我无法理解如何递归函数表达的意思。

其实我只是想定义我的源模型和目标模型。（比如左边三个元素对应右边一个元素；左边一个元素对应右边两个元素）

在阅读有关计算机科学和编程语言的论文时，我经常偶然发现术语指称语义和操作语义。有时，但很少，我也发现公理化的。虽然我知道语义是什么，但我不明白这三者之间的区别——实际的分类是什么？

一些示例将非常有用。