重写逻辑语义学项目的计算机科学实用指南

理论计算机科学电子笔记156（2006）27-56www.elsevier.com/locate/entcs重写逻辑语义学项目Jos'eMeseguerandGrigoreRosu1，2计算机科学系，伊利诺伊大学厄巴纳-香槟分校，厄巴纳，IL 61801，美国摘要重写逻辑是一种灵活的、表达性强的逻辑框架，它以一种新颖的方式统一了指称语义和SOS，避免了它们各自的局限性，并允许非常简洁的语义。tic定义。重写理论的公理包括等式和重写规则这一事实提供了一个非常有用的“抽象旋钮”，以在语义定义中找到抽象和可扩展性之间的正确平衡。 这样的语义定义可以作为解释器直接执行，重写逻辑语言，如Maude，其通用的形式化工具可以用来赋予这些解释器强大的程序分析能力。保留字：程序设计语言的语义学和分析，重写逻辑。1引言重写逻辑规范[32，8]提供了一种简单和表达的方法来开发语言的可执行形式定义，然后可以进行不同的工具支持的形式分析，这一事实现在已经得到了很好的证实[5，58，55，53，34，56，13，47，57，23，21，30，6，35，36，11，10，22，17，48，1，54，19]。事实上，刚才提到的不同作者的论文是对一个集体正在进行的研究项目的贡献，我们称之为重写逻辑语义学项目。这个项目的第一个全球快照但这是一个快速发展的领域，因此，新的发展和讨论1 电子邮件：meseguer@cs.uiuc.edu2 电子邮件：grosu@cs.uiuc.edu1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.10.02728J. Meseguer，G.《理论计算机科学电子笔记》156（2006）27[36]中较少强调的方面使我们值得尝试在这里给出第二个快照。我们认为，使这个项目充满希望的是三个相互关联的事实的结合：(i) 正如1.1节和1.2节所解释的，重写逻辑是一个灵活的、表达性强的逻辑框架，它以一种新颖的方式统一了指称语义和SOS，避免了它们各自的局限性，允许非常简洁的语义定义;(ii) 重写逻辑语义定义可以直接在重写逻辑语言（如Maude [14]）中执行，因此可以成为非常有效的解释器;(iii) Maude LTL模型检查器[20]、Maude归纳定理证明器[15，16]等通用形式化工具以及正在开发的新工具（如语言通用偏序约简工具[22]）允许我们分摊许多编程语言的工具开发成本，因此可以赋予强大的程序分析能力;此外，通用性并不一定意味着不精确：在某些情况下，这样获得的分析优于众所周知的语言专用工具[23，21]。1.1语义：等式与SOS编程语言的两个著名的语义框架是：等式语义和结构操作语义（SOS）。在等式语义学中，形式定义采用语义等式的形式，通常满足Church-Rosser性质。高阶和一阶版本都被证明是有用的形式主义。在这些领域有大量的然而，我们可以提到一些早期的指称语义学论文，如[50，51]和调查[49，40]。类似地，我们提到[60，26，7]早期的代数语义论文，其中一些使用初始代数语义，以及[25]最近的一本书。我们使用更中性的术语等式语义来强调这样一个事实，即（高阶）指称语义和（一阶）代数语义具有许多共同特征，并且都可以被视为共同等式框架的实例。等式语义的优点包括：（1）它具有模型理论，在高阶情况下由域给出的指称语义，并且通常在一阶情况下由初始代数给出;（2）它还具有证明理论，由语义等式的等式归约给出的操作语义;（3）由于有效的高阶函数语言（ML，J. Meseguer，G.《理论计算机科学电子笔记》156（2006）2729Haskell等）和一阶方程语言（ACL 2，OBJ，ASF+SDF等）; （4）有良好的高阶和一阶定理证明支持。然而，等式语义有以下缺点：（1）它非常适合于确定性语言，如传统的顺序语言或纯函数语言，但它非常不适合定义并发语言的语义，除非并发是纯确定性计算;（2）人们可以间接地建模3一些并发方面与设备，如调度器，或懒惰的数据结构，但直接所有并发方面的综合建模在等式框架内仍然是难以捉摸的;（3）语义等式通常是非模块化的，即，向语言中添加新的特性通常需要对早期的语义方程进行广泛的重新定义在SOS中，形式定义采用语义规则的形式。SOS是一种证明理论方法，专注于对程序的执行给出详细的逐步形式化描述语义规则被用作推理规则来推理可能的计算步骤。通常，规则遵循程序的语法结构，根据其部分的语义定义语言构造的语义经典的地方是普洛特金SOS的优点包括：（1）它是一个通用的，但非常直观的形式主义，允许详细的一步一步的程序执行建模;（2）它有一个简单的证明理论语义，使用语义规则作为推理规则;（3）它非常适合于建模并发语言，也可以很好地处理确定性语言的详细执行;（4）它允许数学推理和证明，通过归纳或共归纳推理的推理步骤。然而，SOS具有以下缺点：（1）在其标准公式中，它强加了并发计算的集中式交织语义，这在某些情况下可能是不自然的（例如高度分散和异步的移动计算）;这个问题在“reductionsemantics”中被避免，这与SOS不同，实际上是重写语义的特殊情况（见第2.1节）;（2）标准SOS定义是众所周知的非模块化的，除非采用Mosses的MSOS框架[ 41，42，43 ];（3）尽管已经构建了一些工具来执行SOS定义（例如见[ 18，28，44 ]），但对验证属性的3在纯函数框架内间接建模并发性的两个很好的例子是使用调度器的JVM的ACL 2语义[39]，以及在Haskell中使用惰性数据结构来分析加密协议[2]。30J. Meseguer，G.《理论计算机科学电子笔记》156（2006）271.2统一SOS和等式语义：抽象旋钮在很大程度上，等式语义学和SOS是分开的。语用考虑和品味上的差异往往决定了在每一特定情况下采用哪种对于并发语言来说，SOS显然更优越，并倾向于作为选择的形式主义而流行，但对于确定性语言来说，等式方法也被广泛使用。当然，对于执行和形式化推理的工具支持也有实际的考虑最后，等式语义学和SOS，尽管各自都有其价值，但都是“单锤”方法。是否有可能将它们无缝地统一在一个更加灵活和通用的框架内？当它们如此统一时，它们各自的局限性是否可以克服？我们的建议是，重写逻辑[32，8]确实提供了一个这样的统一框架。这个统一的关键其实非常简单，就是我们所说的重写逻辑关键在于，在等式语义学的模型论方法中在我们的旋钮隐喻中，这意味着在等式语义中，抽象旋钮总是一直转到它的最大位置。 相比之下，SOS的一个关键特性是提供了一个非常详细的，一步一步的语言评估机制的正式描述因此，大多数实体（可能除了通常在侧面处理的内置数据、存储和环境）主要是语法的在我们的比喻中，这意味着在SOS中，抽象旋钮总是被调低到最小位置。如何实现抽象旋钮的统一和相应的可用性？粗略地说，重写理论是一个三元组（E，E，R），其中（E，E）是一个等式理论，其中E是操作和排序的签名，E是一组（可能是条件的）等式，R是一组（可能是条件的）重写规则。等式语义是作为R=E的特殊情况获得的，因此我们只有语义等式E，并且抽象旋钮被转到其最大位置。大致上说，SOS（与未标记的转换）作为E= E的特殊情况获得，并且我们只有（可能有条件的）重写纯语法实体（术语）的规则R，因此抽象旋钮被调低到最小位置。重写逻辑的“抽象旋钮”正是重写理论中方程E和规则R之间的区别（E，E，R）。国家的COM-[4]我们将“等式归约策略”μ和“冻结”的论证信息φ的讨论推迟更详细地说，重写理论将被公理化为元组（tuple，E，μ，R，φ）。J. Meseguer，G.《理论计算机科学电子笔记》156（2006）2731假设是E-等价类，即，初始代数T∈E中的抽象元素。由于重写逻辑然而，旋钮可以向上或向下转动我们可以通过将所有方程转换为规则，将（E，E，R）转换为（E，E，R，E，R），将它一直降到最小这为我们提供了最具体的、类似于SOS的语义描述。一般来说，我们能做些什么来使一个尽可能抽象的具体化，也就是说，尽可能？我们可以确定一个子集R0<$R，使得：（1）R0<$E是Church-Rosser;（2）R0是具有此性质的最大可能在实际的语言规范实践中，这并不难做到。我们举例说明这个想法在3.1节中有一个简单的例子。从本质上讲，我们可以将语义方程用于编程语言的大多数顺序特性：只有当与内存的交互可能导致非确定性（特别是如果语言具有线程，或者它们可以稍后在扩展中添加到语言中）或对于本质上并发的特性，规则（而不是方程）才是真正需要的。方程和规则之间的概念区别对程序分析有着重要的实际意义，因为它意味着大量的状态空间缩减，这可以使形式化分析（如广度优先搜索和模型检查）更加有效。由于状态空间的扩展，如果我们使用一个类似于SOS的规范，其中所有的计算步骤都用规则来描述，那么这样的分析很容易变得不可行这种处理抽象状态的能力是我们的通用工具在实例化到给定的编程语言定义时往往会导致具有竞争力性能的程序分析工具的关键原因当然，交换抽象的代价是更粗的粒度级别，即在该抽象级别上可以观察到计算的哪些方面。例如，当使用语义分析顺序程序时，其中大多数顺序特征已经用等式指定，所有顺序子计算将被抽象掉，分析将集中在内存和线程交互上。如果需要更精细的分析，我们通常可以通过将一些方程转换为规则来“调低抽象旋钮”到正确的可观察性水平来获得它也就是说，我们可以调节旋钮，为每种分析找到抽象性和可观察性之间的最佳平衡。本文的其余部分组织如下。第2节给出了成员关系方程逻辑和重写逻辑的背景。与等式语义和SOS的关系将在2.1节中详细讨论。然后，我们说明了我们的想法，给出一个重写逻辑语义的一个简单的32J. Meseguer，G.《理论计算机科学电子笔记》156（2006）27在3.1节中介绍了编程语言，并在3.2节中总结了其他语言规范的案例研究。程序分析技术和工具在第4节中讨论，包括搜索和模型检查分析（4.1），以及基于抽象语义的分析（4.2）。我们在第5节中做一些总结性的评论。2重写逻辑语义成员资格的逻辑。一个隶属方程逻辑（MEL）[33]签名是一个三元组（K，S，S）（以下简称S），其中K是一个类集，S={S，w，k}（w，k）∈K∈K ×K是一个y-类签名，而S={S，k}k∈K是一个K-k个不相交的类集的索引族。一个类 s 的 种 类 用 [s] 表 示 一 个 梅 尔 代 数 结 构 A 是 一 个 集 合 Ak ，其 中 eachkindk∈K，一个函数Af：Ak1×· · ·×Akn→Akforea choperatorf∈Sk1···kn ， k ， andndasubsetAs<$Akfor eachsort s ∈ Sk，with the meaning that the elements in sort are well defined，而没有排序的元素是错误的。 我们写T，k和T（X）k分别表示X中变量上k类基项和k类基项的集合，其中X ={x1：k1，.，xn：kn}是一组kinded变量。给定一个MEL签名，原子公式具有t=TJ（n-方程）或t：s（n-隶属度）的形式，其中t，TJ∈T<$（X）k，s∈Sk;和-语句是形式为“（X）if i p i =”的条件公式。qijwj：sjx中的变量pi，qi和wj都在X中。 一个MEL理论是一个具有MEL签名的对（E，E），E是一组mel-句子. 我们参考[33]详细介绍了（E，E）-代数，健全和完整的演绎规则，以及初始和自由代数。特别地，给定一个梅尔理论（E，E），它的初始代数记为T/E;它的元素是T中基项的E-等价类。 排序符号s1Name.endfmSIMPLE是一种表达式语言，意味着一切都解析为表达式。如4.2节所述，如果需要，可以在表达式语法之上轻松定义复杂类型检查器通过使用排序，可以直接定义不同的语法类别，例如语句，算术和布尔表达式等。我们首先将表达式一般地定义为扩展名称和Maude整数目前我们不需要/不想知道其他语言稍后将添加结构：fmodGENERIC-EXP-SYNTAX包含NAME。包括INT。排序表达式子排序IntName< Exp.endfm我们现在准备向SIMPLE的语法添加语言特性。我们从添加常见的算术表达式开始：fmodARCHMETIC-EXP-SYNTAX包含GENERIC-EXP-SYNTAX。ops _+_ _-_ _*_：Exp Exp -> Exp [同上]。ops_/__%_：Exp Exp -> Exp[prec 31]。endfm为了节省空间，从这里开始，我们省略了添加整个模块来定义一个特定的功能，但只提到它的重要特征;参见[37]简单的完整定义。接下来让我们添加布尔表达式的语法ops true false：-> Exp.操作_=='__！='_ _<<'_ _'__ ='_ _>='_：Exp Exp -> Exp [prec 37]. op_and_：Exp Exp-> Exp [prec 55].op_or_：Exp Exp-> Exp [prec 59].op not_：Exp-> Exp [prec 53].请注意，在这个阶段，我们不区分算术表达式和布尔表达式。当我们定义SIMPLE的语义时会考虑到这一点。与某些算术运算符相关的属性同上表示它们继承了先前定义的同名运算符的属性;这些运算符与内置的INT模块一起导入当然，内置模块/功能在语言定义中是不必要然而，对于基本的语言特性（如整数运算），重用现有的高效库是非常方便的重载内置运算符实际上很有用，但有时会引起语法/解析问题。例如，在一个示例中，整数上的内置二元关系运算符计算为Bool排序，对于技术和由于个人品味的原因，我们不想将其定义为Exp的子类。因此，我们不能在我们的简单语言中重载这些运算符即我们在上面的模块中为他们的名字添加反引号的原因条件语句几乎对任何编程语言都是必不可少的操作if_then_：Exp Exp -> Exp.op if_then_else_：Exp Exp Exp -> Exp.40J. Meseguer，G.《理论计算机科学电子笔记》156（2006）27命令式和顺序组合是命令式语言的核心特征。与C不同，我们更喜欢使用不那么容易混淆的：=运算符进行赋值（而不是仅仅使用=，许多人认为这是一种糟糕的表示法）：op_：=_：Name Exp-> Exp [prec 41]....op_;_：Exp Exp-> Exp [ascurp prec 100]。属性10表示该操作是关联的。 这是一个本质上的语义属性;然而，我们更愿意将其作为语法的一部分，因为Maude的解析器使用它来消除对括号的需要。在简单的定义中，列表被多次使用：变量和函数声明需要表达式列表，函数调用需要表达式列表，作为程序执行结果的输出需要值列表由于我们在这些不同列表的元素排序之间有一个自然的子排序结构，我们可以以“子类型多态”的风格定义相应的列表我们首先定义列表的基本模块fmod LIST是排序列表。op nil：-> List.op_，_：List List -> List [aslogid：nil prec99]. endfm每次我们需要一个特定排序S的列表时，我们所需要做的就是定义一个扩展上面的排序List的排序SList，以及一个重载的逗号运算符。特别是，我们可以定义如下的名字列表：fmod NAME-LIST包含NAME。包括List。对Name List进行排序。子排序NameList< Name List。op'（'）：-> NameList.op_，_：NameList NameList-> NameList [同上]。eq（）= nil。endfm作为语法糖，请注意我们定义了一个额外的空名称列表操作符（），其语义与nil相同。这是因为在定义或调用没有参数的函数时，我们更喜欢写f（）而不是f（nil）。块允许将多个语句组合成一个语句。此外，块可以定义临时使用的局部变量：用途op {}：-> Exp.op {_}：Exp-> Exp.op {local_;_}：NameList Exp -> Exp [prec 100 gather（e E）]。上面对块的一般定义不仅为用户提供了一个强大的结构，允许在上面声明变量;而且它还将简化以后对函数的定义：函数[10]在Maude中，梅尔理论（mel theory）（E A，μ）或重写理论R中的“模公理”A可以包括结合性、交换性和恒等公理的任何组合。 它们被声明为对应运算符的等式属性，并使用关键字ascurt、idt和id：。然后Maude解释器支持用方程和规则重写模这样的公理。J. Meseguer，G.《理论计算机科学电子笔记》156（2006）2741表达式;如果需要局部变量，那么只需将函数体定义循环和print的语法很简单。我们允许for和while循环：操作（_;_;_）_：Exp Exp Exp Exp-> Exp.操作while：Exp Exp-> Exp.op print_：Exp-> Exp.很快就需要表达式列表来定义函数调用：fmod EXP-LIST包含GENERIC-EXP-SYNTAX。包括姓名列表。对ExpList进行排序。 subsort Exp NameList ExpList [同上]。endfm我们现在准备好定义函数的语法。每个函数都有一个名称、一个参数列表和一个函数体表达式。一个函数调用是一个名字后面跟着一个表达式列表函数可以通过一个典型的return语句强制突然返回如前所述，程序应该提供一个名为main的函数，这是执行开始的地方sort函数opfunction：Name NameList Exp -> Function [prec 115].op：Name ExpList -> Exp [prec 0]。操作返回：Exp-> Exp.op main：-> Name.一个程序可以有更多的函数，这些函数甚至可以是相互递归的。我们为函数集定义语法。我们使用集合是因为它们的顺序根本不重要：每个函数都可以看到其环境中所有其他声明的函数sort FunctionSet。subsort函数 FunctionSet。op：FunctionSet FunctionSet -> FunctionSet [aslogid：empty]。我们希望在SIMPLE中允许动态线程创建，并提供一些适当的同步机制。spawn语句接受任何表达式，并启动一个新线程来计算该表达式。在多线程中，子线程继承了其父线程的环境为了避免竞争条件并允许在我们的语言中进行同步，我们引入了一个简单的基于锁的策略，其中线程可以获取和释放锁：opsspawn_lock acquire_release_：Exp-> Exp.我们已经定义了SIMPLE的所有所需语言特性的语法。现在定义程序语法所需要的就是把所有这些定义放在一起。一个程序由一组全局变量声明和一组函数声明组成fmod SIMPLE-SYNTAX是包括ARMMETIC-EXP-SYNTAX。包括布尔表达式语法。包括IF-SYNTAX。包括分配语法。包括SEQ-COMP-SYNTAX。包括块语法。包括循环语法。包括PRINT-SYNTAX。包括FUNCTION-SYNTAX。包括FUNCTION-SET。42J. Meseguer，G.《理论计算机科学电子笔记》156（2006）27包括线程语法。排序Pgm。subsortFunctionSet Pgm [prec 122].endfm为了测试语法，可以解析稍后想要执行/分析的程序，此时语义也将被定义。根据我们的经验，这是编写数十个基准程序的好时机。简单的国家基础设施。任何实用的编程语言都需要考虑状态的概念。各种语言构造的语义是根据它们如何使用或更改现有状态来定义的因此，在我们继续定义SIMPLE的语义之前，我们需要首先定义它的整个状态基础结构。在我们的方法中，状态可以被看作是一个这里的接下来，我们非正式地描述每种成分，而不给出正式的Maude定义（感兴趣的读者可以参考[37]了解详细信息）：店 存储是位置到值的映射。形式上，定义了一个二进制操作结合与交换运算：StoreStore -> Store以及适当的方程，保证没有两个不同的对同一地点操作<也被定义为商店界面的一部分。每个线程都将包含自己的环境，将名称映射到位置。两个或多个线程可以在它们的环境中访问存储中的同一位置，从而可能导致数据竞争。全球环境。全局环境将每个全局名称映射到相应的位置。全局名称的位置将在执行开始时一次性分配功能协调发展的为了方便（相互）递归函数定义，每个函数都可以看到程序中定义的所有其他函数。实现这一点的一个简单方法是简单地将函数集作为状态的一部分下一个免费的位置。这是一个自然数，给出了存储中可分配值的下一个位置。这是需要的，以便知道在块中的哪里为局部变量分配空间请注意，在本文中，我们不考虑垃圾收集（否则，需要为下一个空闲位置提供更复杂的模式输出. 用print语句打印的值被收集在输出列表中.这份名单将是对该方案进行评估的结果J. Meseguer，G.《理论计算机科学电子笔记》156（2006）2743锁很忙SIMPLE中的线程同步是基于锁的。锁可以由线程获取或释放。但是，如果一个锁已经被一个线程占用，那么任何其他获取相同锁的线程都会被阻塞，直到第一个线程释放该锁。因此，我