操作语义、指称语义和公理语义之间的区别是什么



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

举个例子会非常有用。

这直接出自这本精彩的书的序言"程序设计语言的形式语义;Glynn Winskel著(麻省理工学院出版社,1993年(:

操作语义通过指定编程语言在抽象机器上的执行方式来描述编程语言的含义。我们集中讨论Gordon Plotkin在奥胡斯关于";结构操作语义";其中评估和执行关系由规则以语法指导的方式指定。

指称语义是一种定义编程语言含义的技术,由Christopher Strachey开创,并由Dana Scott提供了数学基础。曾一度被称为";数学语义;它使用了更抽象的数学概念,如完全偏序、连续函数和最小不动点。

公理化语义试图通过在程序逻辑中为编程结构提供证明规则来固定其含义。与这种方法相关的主要名称是R.W.Floyd和C.A.R.Hoare。因此,公理化语义从一开始就强调正确性的证明。

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

如果你能接触到Winskel的书,我强烈建议你通读它,因为它提供了对所有三种技术的详细但非常容易理解的描述。

相关内容

最新更新