formal-semantics - 什么是 "formal semantics"？

Question

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

Giotto has a formal semantics that specifies the meaning of mode switches, of intertask communication, and of communication with the program environment.

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

Answer 1

为了稍微扩展 Michael Madsen 的回答，一个例子可能是++ 运算符的行为。非正式地，我们使用简单的英语来描述运算符。例如:

If x is a variable of type int, ++x causes x to be incremented by one.

(我假设没有整数溢出，并且 ++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有值 -5351 .

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

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

有点非正式，通过执行 ++x ，下一个命令是 skip ，没有作用，store中的变量不变，除了 x ，它现在具有它最初的值加一。还有一些工作要做，例如定义我用于更新商店的符号(我没有这样做是为了阻止这个答案变得更长!)。因此，一般规则的一个特定实例可能是:

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

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

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