我正在阅读一篇非常愚蠢的论文，它一直在谈论 Giotto 如何定义“形式语义”。
Giotto 有一个正式的语义，它指定了模式切换、任务间通信以及与程序环境通信的含义。
我处于边缘，但无法完全理解“形式语义”的含义。
【问题讨论】：
标签： formal-semantics
为了稍微扩展 Michael Madsen 的回答，一个示例可能是 ++ 运算符的行为。非正式地，我们使用简单的英语描述运算符。例如：
如果
x是int类型的变量，++x会使 x 加一。
（我假设没有整数溢出，并且 ++x 不返回任何内容）
在形式语义（我将使用操作语义）中，我们还有一些工作要做。首先，我们需要定义类型的概念。在这种情况下，我将假设所有变量都是int 类型。在这种简单的语言中，程序的当前状态可以用存储来描述，存储是从变量到值的映射。例如，在程序的某个时刻，x 可能等于 42，而y 等于 -5351。商店可以用作函数——例如，如果商店s 的变量x 的值为42，那么s(x) = 42。
程序的当前状态还包括我们必须执行的程序的剩余语句。我们可以将其捆绑为<C, s>，其中C 是剩余的程序，s 是商店。
所以，如果我们有状态<++x, {x -> 42, y -> -5351}>，这是一个非正式的状态，其中唯一剩余要执行的命令是++x，变量x 的值为42，变量y 的值为@987654338 @。
然后我们可以定义从程序的一种状态到另一种状态的转换——我们描述当我们在程序中执行下一步时会发生什么。所以，对于++，我们可以定义如下语义：
<++x, s> --> <skip, s{x -> (s(x) + 1)>
有点通俗点，通过执行++x，下一个命令是skip，没有任何作用，并且store中的变量没有变化，除了x，它现在有原来的值加上一。还有一些工作要做，例如定义我用于更新商店的符号（我没有这样做来阻止这个答案变得更长！）。因此，一般规则的一个具体实例可能是：
<++x, {x -> 42, y -> -5351}> --> <skip, {x -> 43, y -> -5351}>
希望这能给你这个想法。请注意，这只是形式语义的一个示例——除了操作语义，还有公理语义（通常使用 Hoare 逻辑）和指称语义，可能还有很多我不熟悉的。
正如我在对另一个答案的评论中提到的，形式语义的一个优点是您可以使用它们来证明程序的某些属性，例如它终止。除了显示您的程序没有表现出不良行为（例如不终止）外，您还可以通过证明您的程序符合给定规范来证明您的程序按要求运行。话虽如此，我从来没有发现指定和验证程序的想法令人信服，因为我发现规范通常只是用逻辑重写的程序，因此规范很可能是错误的。
【讨论】：
Formal semantics 以一种形式化的方式描述语义——使用以明确的方式表达事物含义的符号。
它与informal语义相反，后者本质上只是用简单的英语描述一切。这可能更容易阅读和理解，但它可能会产生误解，这可能会导致错误，因为有人没有按照您希望他们阅读的方式阅读段落。
一种编程语言可以同时具有正式和非正式语义 - 非正式语义将作为正式语义的“纯文本”解释，如果您不确定什么是正式语义，则可以查看非正式的解释确实意味着。
【讨论】：
就像语言的语法可以用形式语法来描述（例如BNF），可以使用不同种类的形式将语法映射到数学对象（即语法的含义）。
A Practical Introduction to Denotational Semantics 中的This page 很好地介绍了 [指称] 语义如何与语法相关。本书的开头还简要介绍了形式语义的其他非指称方法（尽管维基百科链接Michael 给出了更详细的信息，并且可能是最新的）。
语义模型没有 流行到与 BNF 相同的程度 及其后代有语法。 这可能是因为语义确实 似乎比 句法。最成功的系统是 指称语义描述 命令式中的所有功能 编程语言和声音 数学基础。 （还有 积极研究类型系统和 并行编程。）许多 指称定义可以是 作为口译员执行或翻译 进入“编译器”，但这还没有 导致高效的发电机 编译器可能是另一个原因 指称语义较少 比 BNF 受欢迎。
【讨论】：
在像乔托这样的编程语言的上下文中，这意味着一种具有形式语义的语言，对其各个语言结构具有数学上严格的解释。
当今的大多数编程语言都没有严格定义。它们可能遵守相当详细的标准文档，但最终编译器的责任是生成以某种方式遵守这些标准文档的代码。
另一方面，当需要使用例如模型检查或定理证明对程序代码进行推理时，通常会使用正式指定的语言。适合这些技术的语言往往是函数式语言，例如 ML 或 Haskell，因为它们是使用数学函数和它们之间的转换来定义的；也就是数学的基础。
另一方面，C 或 C++ 由技术描述非正式地定义，尽管存在将这些语言的各个方面形式化的学术论文（例如，Michael Norrish：C++ 的形式语义，https://publications.csiro.au/rpr/pub?pid=nicta:1203），但通常不会找到进入官方标准的途径（可能是由于缺乏实用性，尤其是难以维护）。
【讨论】：