程序设计语言语义

程序设计语言语义计算机术语01简介操作语义公理语义学语义指称语义代数语义目录0305020406基本信息语法和语义是定义一个程序设计语言所涉及的两个重要侧面：语法涉及程序文法结构，研究程序设计语言所允许的成分结构形式；而语义则涉及文法上正确的程序的含义，研究语言与其所指对象间的关系。程序设计语言语义是为了指明给出程序设计语言的程序含义。程序设计语言语义一般分为指称语义、操作语义、代数语义和公理语义学。简介简介程序设计语言，也称编程语言（programminglanguage），是用来定义计算机程序的形式语言。它是一种被标准化的交流技巧，用来向计算机发出指令。程序设计语言语义为了指明给出程序设计语言的程序含义，研究语言与其所指对象间的关系。程序设计语言语义属于形式语义学，在计算理论中，形式语义学是计算的模式和程序设计语言的含义的严格的数学研究的领域。语言的形式语义是用数学模型去表达该语言描述的可能的计算来给出的。形式语义学（formalsemantics），是程序设计理论的组成部分，以数学为工具，利用符号和公式，精确地定义和解释计算机程序设计语言的语义，使语义形式化的学科。语义语义模型论的基本概念之一。指语言表达式和表达式的意义之间的关系。研究语义的理论称为语义理论，又称语义学。语义学不像语法学那样只关心表达式的形式而不关心它们的意义

。而是充分地考虑这些语言表达式在自然语言中的意义以及它们之间的关系。在语义学概念中，有真值、指派、可满足、有效模型等概念。语义学研究系统中公式的意义、系统的解释，且与模型论相关。语言表达式间的语义推论关系用符号⊨表示。例如，赋值语句C=A+B的语义是，把赋值号右边的表达式A+B的值作为赋值左边的变量C的值。在编译过程中不但要对源程序的语法检查其正确性，也要对语义进行检查，保证语义上的正确。在编译程序中，语义分析程序是由许多加工处理子程序组成，其中很重要的一部分是对标识符的处理。操作语义操作语义操作语义通过规定程序设计语言在抽象机器上的执行过程来描述程序设计语言的含义，即用语言的实现方式定义语言的语义，也就是将语言成分所对应的计算机操作作为语言成分的语义。操作语义一般指结构化操作语义(SOS)，又称“小步语义”，其显著特征是：在程序运行过程中，程序短语不断地被替换成所计算的值。这种状态转换可用相应的公理和推导规则来描述。SOS已被广泛用于程序分析和形式化验证等领域。与SOS对应的另一种操作语义为自然语义,亦称“大步语义”,它较SOS隐藏了更多执行细节，只包含初始和最终状态，没有中间状态。自然语义也用公理和推导规则描述计算,只是它不能用于不确定的程序和交叉存取的表达式计算。自然语义已被用于定义SML、Eiffel和Java等语言的语义

。指称语义指称语义在计算机科学中，指称语义（英语：Denotationalsemantics）是通过构造表达其语义的(叫做指称(denotation)或意义的)数学对象来形式化计算机系统的语义的一种方法。编程语言的形式语义的其他方法包括公理语义和操作语义。指称语义方式最初开发来处理一个单一计算机程序定义的系统。后来领域扩展到了由多于一个程序构成的系统，比如络和并发系统。指称语义起源于克里斯托弗·斯特雷奇和DanaScott在1960年代的工作。在Strachey和Scott最初开发的时候，指称语义把计算机程序的指称(意义)解释为映射输入到输出的函数。后来证明这对于允许包含递归定义的函数和数据结构这样的元素的程序的指称(意义)定义太受限制了。为了解决这个困难，Scott介入了基于域的指称语义的一般性方法(AbramskyandJung1994)。后来的研究者介入了基于幂域的方法，来解决并发系统的语义的问题(Clinger1981)。粗略的说，指称语义找到代表程序所做所为的数学对象。这种对象的搜集叫做域。例如，程序(或程序段)可以被偏函数，或演员事件图想定，或在环境和系统之间的博弈表示:它们都是域的一般性例子。指称语义的一个重要原则是“语义应当是复合性的”:程序段的指称应当创建自它的子段的指称。最简单的例子是:“3+4”的意义确定自“3”、“4”和“+”的意义。指称语义最初被开发为把函数式和顺序式程序建模为映射输入到输出的数学函数的框架。公理语义学公理语义学公理语义学（Axiomaticsemantics）是使用数理逻辑来证明程序正确性。程序中的命令的意义描述是通过对程序状态的断言（assertion）效果。断言是逻辑语句——带变量的谓词，而这些变量定义了程序的状态。公理语义的应用也非常广泛，早在1973年,.Hoare和N.Wirth就给出了Pascal完整的公理语义；随后,其他研究者给出了一些面向对象程序设计语言(如Java)的核心子语言和语义描述语言(如XML)的公理语义和程序验证。代数语义代数语义代数语义用代数方法对形式语言系统进行语义解释,即用代数公理刻画语言成分的语义，且只研究抽象数据类型的代数规范。抽象数据类型的代数规范通过构造算子和一组有关运算的代数公理刻画类型操作的行为。抽象数据类型的语法称为基调，一个基调由它的类子集(基本语法元素)和运算集(语法元素间的组合关系)两部分组成。在论证这种规范满足协调性和完全性的基础上，通过寻找