formal-semantics - 什么是“形式语义”？

Question

我正在阅读一篇非常愚蠢的论文，它一直在谈论乔托如何定义“形式语义”。

Giotto 有一个正式的语义，它指定了模式切换、任务间通信以及与程序环境通信的含义。

我处于边缘，但无法完全理解“形式语义”的含义。

Answer 1

为了稍微扩展迈克尔·马德森的回答，一个例子可能是 ++ 运算符的行为。非正式地，我们使用简单的英语描述运算符。例如：

如果x是 类型的变量int，则++x使 x 加一。

（我假设没有整数溢出，并且++x不会返回任何内容）

在形式语义（我将使用操作语义）中，我们还有一些工作要做。首先，我们需要定义类型的概念。在这种情况下，我将假设所有变量都是 type int。在这种简单的语言中，程序的当前状态可以用存储来描述，存储是从变量到值的映射。例如，在程序中的某个时刻，x可能等于 42，而y等于 -5351。store 可以用作函数——例如，如果 stores有值为 42 的变量x，则s(x) = 42.

程序的当前状态还包括我们必须执行的程序的剩余语句。我们可以将其捆绑为，剩余程序<C, s>在哪里，商店在哪里。Cs

因此，如果我们有 state <++x, {x -> 42, y -> -5351}>，这是一个非正式的状态，其中唯一剩余的要执行的命令是++x，变量x的值为 42，变量y的值为-5351。

然后我们可以定义从程序的一种状态到另一种状态的转换——我们描述当我们在程序中进行下一步时会发生什么。因此，对于++，我们可以定义以下语义：

<++x, s> --> <skip, s{x -> (s(x) + 1)>

有点非正式地，通过执行++x，下一个命令是skip，它没有任何效果，并且存储中的变量没有变化，除了x，它现在具有它最初的值加一。还有一些工作要做，例如定义我用于更新商店的符号（我没有这样做来阻止这个答案变得更长！）。因此，一般规则的一个特定实例可能是：

<++x, {x -> 42, y -> -5351}> --> <skip, {x -> 43, y -> -5351}>

希望这能给你这个想法。请注意，这只是形式语义的一个示例——除了操作语义之外，还有公理语义（通常使用 Hoare 逻辑）和指称语义，可能还有很多我不熟悉的。

正如我在对另一个答案的评论中提到的那样，形式语义的一个优点是您可以使用它们来证明程序的某些属性，例如它终止。除了显示您的程序没有表现出不良行为（例如不终止）外，您还可以通过证明您的程序符合给定规范来证明您的程序按要求运行。话虽如此，我从来没有发现指定和验证程序的想法如此令人信服，因为我发现规范通常只是用逻辑重写的程序，因此规范很可能是错误的。

Answer 2

形式语义学以一种形式化的方式描述语义，使用以明确方式表达事物含义的符号。

它与非正式语义相反，后者本质上只是用简单的英语描述一切。这可能更容易阅读和理解，但它可能会产生误解，这可能会导致错误，因为有人没有按照您希望他们阅读的方式阅读段落。

一种编程语言可以同时具有正式和非正式语义 - 然后非正式语义将用作正式语义的“纯文本”解释，如果您不确定非正式解释是什么，正式语义将是查看的地方真正意思。

Answer 3

就像语言的语法可以用形式语法（例如BNF）来描述一样，可以使用不同种类的形式将语法映射到数学对象（即语法的含义）。

来自A Practical Introduction to Denotational Semantics的这一页很好地介绍了 [denotational] 语义如何与语法相关。本书的开头还简要介绍了形式语义的其他非指称方法（尽管迈克尔给出的维基百科链接更加详细，并且可能是最新的）。

来自作者的网站：

语义模型没有像 BNF 及其后代在语法上那样流行。这可能是因为语义似乎确实比语法更难。最成功的系统是指称语义，它描述了命令式编程语言中的所有特性，并具有良好的数学基础。（在类型系统和并行编程方面仍然有积极的研究。）许多指称定义可以作为解释器执行或翻译成“编译器”，但这还没有导致高效编译器的生成器，这可能是指称语义不太受欢迎的另一个原因比 BNF。

Answer 4

在像乔托这样的编程语言的上下文中，这意味着一种具有形式语义的语言对其各个语言结构具有数学上严格的解释。

今天的大多数编程语言都没有严格定义。它们可能遵循相当详细的标准文档，但最终编译器的责任是生成以某种方式遵循这些标准文档的代码。

另一方面，当需要使用例如模型检查或定理证明对程序代码进行推理时，通常使用正式指定的语言。适合这些技术的语言往往是函数式语言，例如 ML 或 Haskell，因为它们是使用数学函数和它们之间的转换来定义的；也就是数学的基础。

另一方面，C 或 C++ 由技术描述非正式地定义，尽管存在正式化这些语言方面的学术论文（例如，Michael Norrish：C++ 的形式语义，https://publications.csiro.au/rpr/pub ?pid=nicta:1203），但这通常不会进入官方标准（可能是由于缺乏实用性，尤其是难以维护）。