指称语义

发布时间 2023-11-28 20:16:13作者: DennyQi

一段程序在形式上只是一个符号串,程序的语义是人对程序意义的理解。现在我们希望严格化地定义这种理解。下面要讨论的这种方式称为“指称语义”。

表达式的指称语义

整数类型表达式

首先定义表达式的指称语义,这里我们只考虑由常数、变量、四则运算构成的表达式。首先我们不考虑变量的范围,并认为变量只能取整数,这样任何时候一个表达式的语义应当都是一个整数。同时,表达式的语义只取决于所有变量的取值。我们可以定义一个称为“程序状态”的概念,自然地,程序状态就是某一时刻所有变量的取值,它在本质上是一个从变量名到\(\Z\)的映射。由此定义常量的指称语义就是常量,变量的指称语义是当前程序状态上变量的值,四则运算递归定义。 表达式的化简其实就是表达式的等价变换,所谓等价根据指称语义的定义就应当是两个表达式的值在任何程序状态下都相等。

布尔表达式

布尔表达式是一类特殊的表达式,它不同于上面定义的整数表达式,它只有真假两种取值。布尔表达式可以看作整数类型表达式复合上与或非及其它二元运算符以后的新表达式,自然地只需要在定义true和false以后递归定义即可。

程序语句的指称语义

表达式是在某一程序状态下一个符号串映射的值,而程序语句在执行前后将可能改变程序状态。于是,在指称语义中程序语句的语义就被定义为执行前后程序状态\(s_1,s_2\)的所有可能的二元组。枚举所有可能的\(s_1\),在执行语句后得到\(s_2\),程序语句的语义就是所有这些二元组\((s_1,s_2)\)。空语句就是所有相同程序状态构成的二元组,赋值语句是所有把赋值变量修改成了特定值以后的二元组,顺序执行语句就是两个二元关系的复合,if语句是条件表达式的真假(相当于取子集,而子集也是一种特殊的二元关系)复合上对应的语句。while语句的语义比较复杂,它可以被定义为无穷的并集,也可以在写出表达式后被定义为一个函数的不动点,我们采用后者的定义。

现实程序语言的指称语义

在现实中,整数类型表达式是由范围限制的。因此当表达式的值越界时,应当返回求值出错。一种直接的做法是,将表达式的值域定义为\(\Z_{2^{64}} \cup \{\epsilon\}\),其中\(\epsilon\)表示越界。在做表达式的四则运算时,也要先判断是否越界再做运算。另一种做法是把表达式的指称语义定义为程序状态与表达式的值的二元关系\((s,n)\),如果越界则为空集。这样定义之后,表达式的指称语义就分为normal和error两种情况。

由于表达式求值可能出错,因此程序语句的语义中也应当包含出错。同时,程序语句也可能出现while循环死循环的情况。因此语句的语义可以分为normal、error和inf三种情况。程序语句的指称语义依然是二元关系的集合。