操作语义、表示语义和公理语义之间有什么区别？

Question

在阅读有关计算机科学和编程语言的论文时，我经常在术语、表示语义和操作语义上绊脚石。有时，但很少，我也找到了公理。虽然我知道什么是语义，但我不知道这三个- what之间的区别是实际的分类吗？

有些例子将是非常有用的。

Answer 1

这是一本精彩的书“编程语言的形式语义学”的序言，作者是Glynn Winskel (麻省理工学院出版社，1993年)：

操作语义通过指定编程语言在抽象机器上的执行方式来描述编程语言的含义。我们集中于Gordon Plotkin在奥胡斯关于“结构操作语义”的讲座中所提倡的方法，在该方法中，评估和执行关系是由规则以语法指导的方式指定的。

转换语义是一种定义编程语言含义的技术，由Christopher开创，Dana Scott提供了一个数学基础。它曾经被称为“数学语义”，它使用了完全偏序、连续函数和最小不动点等更抽象的数学概念。

公理语义学试图通过在程序逻辑中给出程序构造的证明规则来修正编程结构的意义。与此方法相关的主要名称是R.W.Floyd和C.A.R.Hoare。因此，公理语义学从一开始就强调正确性的证明。

因此，这些是不同的方法来推理程序的意义，其总体目标是能够证明特定的程序“正确”工作。它们并不是对立的:每一种技术都有其用途，而且常常可以一起用于研究各个方面。例如，在对Haskell进行推理时，通常对纯片段(本质上是递归函数)使用一种表示方法，并使用一种操作方法来推理IO和并发性。典型的命令式语言(Pascal或C类)通常使用公理语义以最弱先决条件的形式推理正确性。

我强烈建议阅读Winskel的书，如果你能掌握它，因为它提供了一个详细的，但非常容易访问的帐户，所有三种技术。