MSVL中结构体以及结构体指针类型的扩展解释系统及其扩展方法

摘要

本发明公开了一种MSVL中结构体以及结构体指针类型的扩展解释系统，具体包括结构体类型定义模块、结构体变量定义声明模块、结构体变量存储模块和结构体及结构体指针类型赋值操作处理模块；在该系统的基础上，还公开了一种MSVL中结构体以及结构体指针类型的扩展方法，该方法在MSVL基本数据类型(包括整型、浮点型、字符型、字符串型)和指针类型的基础之上扩展了结构体类型和相应的结构体指针类型，解决了现有MSVL中数据类型单一，应用范围窄的问题，使得MSVL可用于相对复杂的多数据类型系统的建模、仿真和验证。

说明书

技术领域

本发明属于计算机系统形式化建模与验证技术领域，主要涉及一种MSVL中 结构体以及结构体指针类型的扩展解释系统及其扩展方法。

背景技术

在诸如数字电路和软件工程等形式化验证领域，时序逻辑已经逐渐成为描 述和推理并发系统性质的有效工具。投影时序逻辑(PTL)扩展了区间时序逻辑 (ITL)，并且被广泛运用于系统说明和验证中。大多数情况下，系统建模技术 和时序逻辑无关，但是系统所期望的性质却是用时序逻辑公式来描述的。所以， 就导致了系统验证出现这样一个问题，系统建模和性质描述采用了不同的形式 化方法，而不同的形式化方法有不同的表达式和语义，于是就容易造成混淆。 为了改善这一现状，可以用同一种时序逻辑语言对系统进行建模和性质描述。 MSVL是一种用于建模、仿真和验证程序的投影时序逻辑程序设计语言，它是PTL 的一个可执行子集。我们可以用MSVL程序来对一个系统建模，并且用命题投影 时序逻辑(PPTL)公式来描述该系统的性质，最终在同一个时序逻辑框架下进 行模型检测，来验证系统所期望的性质是否满足。

在编程语言中引入类型是很重要的，它可以让程序员写出更加合理和实用 的程序，众所周知，大多数传统编程语言，例如C和Java都有自己的数据类型， 包括整型、数组、列表、指针和结构体等等。同样地，在时序逻辑编程语言中 引入这些类型也是非常重要的，这样程序员不但可以写出更加合理和实用的程 序，并且可以用来验证包含复杂类型的系统。但是，现在大多数时序逻辑语言， 例如TLA和METATEM都还不支持类型。在TLA中，TLA+规范语言和PlusCal算 法语言本质上是无类型的，其中类型正确性被简单地当作一个不变量，可以用 TLC来验证。METATEM是一个面向代理的编程语言，它的类型仅仅适用于代理， 用来确保确定的行为规范是满足的。这些语言中的类型概念和传统语言中变量 或者表达式的类型概念大不相同。研究投影时序逻辑语言实现类型的技术，尤 其是MSVL语言中的类型实现，可以大大缩小投影时序逻辑语言和传统语言之间 的差距。

目前，在MSVL中已经有了基本数据类型，包括整型、浮点型、字符型、字 符串型和基本指针类型，但是，只有基本数据类型和指针类型不足以对一些复 杂数据系统进行建模、仿真和验证。为此，本发明在MSVL基本数据类型和指针 类型的基础上扩展了结构体以及相应的结构体指针类型，使得MSVL的数据类型 更加完整，可以运用在数据类型更加复杂的系统中，随着类型的发展，现在可 以把更多的C程序翻译成类型化的MSVL程序，并且可以在MSVL解释器工具中 进行建模、仿真和验证。

发明内容

针对现有技术的不足，本发明旨在提供一种MSVL中结构体及结构体指针类 型的扩展解释系统及其扩展方法，在MVSL基本数据类型和指针类型的基础上， 扩展结构体以及结构体指针类型，使得MSVL可以运用在包含更加复杂的数据类 型的系统中，对系统进行建模、仿真和验证，也使得MSVL和传统编程语言之间 的差距减小，使得MSVL更加的实用。

为了实现上述目的，本发明采用如下技术方案：

MSVL中结构体及结构体指针类型的扩展解释系统，包括如下模块：

结构体类型定义模块：所述结构体类型定义模块包括结构体类型的定义；

结构体变量定义声明模块：所述变量定义声明模块包括所述变量声明命令 以及类型声明定义；

结构体变量存储模块：所述变量存储模块包含有变量类型标记和变量取值， 所述变量类型标记根据变量声明语句记录该变量的类型，变量存储两边的取值 限制在其类型所对应的论域内；

结构体及结构体指针类型赋值操作处理模块：赋值操作的左操作数为变量， 右操作数为表达式并对左操作数进行解释。

一种基于上述系统的MSVL中结构体及结构体指针类型的扩展方法，具体包 括如下步骤：

步骤1，对于MSVL中的基本数据类型引入指针类型；所述MSVL中的基本数 据类型包括整型、浮点型、字符型、字符串型；

步骤2，在指针类型的基础上，引入结构体类型，扩展出结构体及结构体指 针类型；通过所述结构体类型定义模块，并结合结构体类型定义的条件，给出 正确的结构体类型定义；

步骤3，通过所述结构体变量定义声明模块，用MSVL中的类型声明语句定 义结构体变量，并声明所述结构体类型以及结构体指针类型；引入类型后，每 个变量都是先声明再引用，声明规定了变量的类型，这样在其他语句中引用时， 可以直接对变量进行解释获取变量的值的类型，从而提高程序执行的效率。

步骤4，通过所述结构体变量存储模块，根据所述结构体变量所声明的类型 及其语义，将所述结构体变量保存在MSVL符号表中，所述MSVL符号表为存放 MSVL变量的表；

步骤5，在所述结构体及结构体指针类型赋值操作处理模块中对所述结构体 类型以及结构体指针类型进行赋值操作。

需要说明的是，所述步骤1中在基本数据类型中引入指针类型具体流程如 下：

步骤1.1，所述基本数据类型集合用表示，其中包括原始数据类型int  float char、列表类型int<>float<>char<>、数组类型int[]float[]char[]； 由于在类型声明时，定义一个数组需要给定数组长度，比如：int[a]5，因此给 定数组长度后的基本数据类型的集合用表示，定义如下：

int[1]，int[2]，...，float[1]，float[2]，...，char[1]，char[2]，...}；

并给出所述基本数据类型的论域

Float[]∪Char∪Char<>∪Char[]；

其中：

步骤1.2，用Is_T定义表示一种基本数据类型，其中从而可以得到类 型声明公式：

步骤1.3，定义一个解释I[e]来表示变量e类型化的值，其中nil表示变量还未定义；

例如：I[8]＝(8，int)，I[<′x′，′y′>]＝(<′x′，′y′>，char<>)。

步骤1.4，对于每一种基本数据类型，引入指针类型，记作T*，而指针类型的 集合用表示；

指针类型的解释需要一个合适的地址模型，因此把指针t解释为(x，int)， 表示指针t指向变量x，而*t解释为x；

步骤1.5，定义指针类型的论域如下：

其中，代表所有变量名的集合，NULL是一个空指针；如果指针t为空指 针，t的解释I[t]＝(NULL，T*)，否则I[t]＝(x，T*)；

步骤1.6，定义指针的基本操作引用(&)和解引用(*)如下：

空指针在程序中是非常有用的，所以MSVL中，也允许NULL_T*在程序中出现， 其中因为每一个表达式要有确定的类型，所以下标T*一般情况不能省 略。只有在省略后不引起歧义的情况下才可以省略；

例如：t₁和t₂分别代表int*和char*那么公式t₁＝NULL_int*∧t₂＝NULL_char*可以简 写为t₁＝NULL∧t₂＝NULL，这样我们不可能误以为是t₁＝t₂。

步骤1.7，在基本数据类型，已经定义用Is_T(·)来表示一种T类型，现在把指 针类型扩展进去；对于每一个指针类型，定义如下：

并且

其中，是bool类型，上式解释为，如果变量v是T类型，则为true，否 则为false；

步骤1.8，如下定义指针类型变量的声明：

其中，

示例说明：

如图2所示，用指针实现三个整数从大到小的排序。

示例代码：

function swap(int*p1，int*p2)

//swap two variables using pointers

{frame(n)and(int n and skip；

n：＝*p1；*p1：＝*p2；*p2：＝n)}；

{frame(n1，n2，n3，p1，p2，p3)and(

int n1，n2，n3and skip；

int*p1，*p2，*p3and skip；

input(n1，n2，n3)and skip；

p1：＝&n1；p2：＝&n2；p3：＝&n3；

if(n1＞n2)then{swap(p1，p2)}else{skip}；

if(n2＞n3)then{swap(p2，p3)}else{skip}；

if(n1＞n3)then{swap(p1，p3)}else{skip}；)

需要说明的是，所述步骤2中具体流程如下：

步骤2.1，在指针类型的基础上引入结构体类型，用S表示结构体类型，表示一个可数的结构体类型集合，则有对每一种结构体类型，用S*表示 结构体类型S的指针类型，则所述结构体中指针类型的集合为

步骤2.2，初步定义结构体为：

struct S{T₁a₁，...，T_ka_k]；

其中(\表示除去)，为所有变量名的集合， 为基本数据类型的集合，为指针类型的集合；所述结 构体类型S中的每一个成员a_k分别对应类型T_k；

为了简化这个理论，不允许结构体嵌套，但是允许一个结构体成员的指针 指向另一个结构体类型。这样，就可以容易地定义链表、树和图等复杂数据类 型。

步骤2.3，一旦定义好一个结构体类型S，就可以用Sx来声明一个新的结构 体类型变量，因此x就拥有的所有成员类型，可以用x.a来表示的每一个成员； 同样还可以定义一个结构体指针类型S*t，其中用t-＞a来指向结构体的 成员a，结构体指针类型S*t为空指针，把t解释为(NULL，S*)，否则，把t 解释为(x，S*)；综上所述，结构体指针类型的论域定义如下：

步骤2.4，结构体类型定义为struct S{T₁a₁，...，T_ka_k]，对于每一个类型的变量x把 它解释为其中对于x的论域其实就是它每 一个成员变量论域的集合，其中涉及到基本数据类型域指针类型域或者 结构体指针类型域综上所述，结构体类型的论域定义如下：

可以得出为一个嵌套的二元组，其中FPF(E₁，E₂)表示从集合E₁到集合E₂所有 的有限偏函数，如下定义FPF：

其中，E是有限的，并且如果(u，v)，(u，v′)∈E，那么v＝v′，即u和v是一 一对应的；

结构体的基本操作是结构体成员的存取。对每一个成员a表示结构体 成员的名字。定义“.a”来进行成员的存取操作。例如：假定e是一个结构体类型， 而a是它的一个成员，那么e.a就返回成员a。

所以，就有了如下定义：

之前在指针类型部分定义过一般指针的引用和解引用操作，对于结构体指 针类型同样适用。例如：假定t是一个指向结构体a的结构体指针类型，用t-＞a 就可以返回a。

所以，就有了如下定义：

和基本数据类型指针一样，在程序中我们也允许结构体指针类型为空，表 示为NULL_T*，其中

结合之前的基本数据类型指针，我们可以把NULL_T*解释为(NULL，T*)，其中， 同样的，当下标T*省略不会引起歧义时可以省略。

步骤2.5，对于基本数据类型和指针类型有现在对其进行扩展， 把结构体类型引入就得到并且对于每一个都有：

并且

步骤2.6，由于结构体类型的复杂性，用逻辑公式来进行结构体的形式化定 义和变量声明并不是一件容易的事，所以不得不考虑一些细节问题：

首先，要考虑结构体类型定义不合法的可能性。用下面的定义：

来声明结构体S的成员。这种情况下，规定如果S_i(1≤i≤m)的定义不迟于结 构体S的定义，结构体S的定义就是合法的。否则，就不合法。

例如：在程序struct S₁{int a}∧○(struct S₂{S₁*a₂})中，S₁在S₂之前定义，所以S₂是合 法的。另外一个程序struct S₁{S₂*a}∧struct S₂{S₁*a₂}中，因为S₁和S₂是同时定义的， 所以也是合法的。对于如何处理不合法的结构体类型定义，一种自然的想法就 是让包含有不合法结构体类型定义的不健康程序不可满足，也就是说该程序不 合法。

但是，这种方法不可行。对于程序struct S₂{S₁*a₂}来说，它本身就是不健康的 程序，也就是说如果struct S₂{S₁*a₂}是不满足的，那么struct S₁{S₂*a₁}∧struct S₂{S₁*a₂} 也就是不满足的，但是实际又是满足的，这就产生了矛盾。

为了解决这个矛盾，引入系统变量healthy，所述系统变量healthy为字符 类型变量；所述变量healthy只有y和n两个值，默认值为y(yes)，在一些 坏情况下设置为n(no)；由于不允许在程序中出现一个显示的系统变量，所以 要求程序员不能修改healthy变量的值。为了处理这些不健康的程序，充分利 用系统变量healthy重新规范地定义结构体如下：

其中

步骤2.7，对于每一个结构体类型S，引入r_s表示它是否定义过：结构体类 型S一旦定义，r_s就一直保持是true，只有S未定义前是false；这是因为遵循 MSVL极小模型语义的规则。在极小模型语义中，一个命题独立于其他命题可以 为真，也可以为假时，它被解释为false；如果struct S{T₁a₁，...，T_ka_k]是不合法的， 那么在当前状态为false，并且把变量healthy的值设置为n；

步骤2.8，在结构体变量x拥有结构体类型S同样的成员以及类型时，则认为 结构体变量x和结构体类型S是一致的，即：

当结构体S定义为struct S{T₁a₁，...，T_ka_k]时，x被解释为其中

步骤2.9，为了确保结构体变量及其成员的一致性，在结构体变量定义时记 录它每个成员的信息，然后用来限制每一个结构体变量，因此引入一个系统变 量mem_s定义为：

这样得到一个特殊类型：

其中MEMTYPE是用来记录结构体每个成员的信息；

步骤2.10，得出结构体S的最终定义：

其中，当k＝0时，{(a₁，T₁)，...(a_kT_k)}是空集

需要说明的是，所述步骤3的具体流程为：

步骤3.1，所述结构体变量定义为一个嵌套的二元组；

步骤3.2，为了检查结构体变量和定义的一致性，定义一个断言Con_s用 Con_s(x，mem_s)表示一致；对于每一个并且{(a₁，T₁)，...(a_kT_k)}∈MEMTYPE，都有：

并且

当且定当有

步骤3.3，结合所述变量healthy给出结构体类型以及结构体指针类型的声 明如下：

如果一个结构体变量声明Sx是合法的，一旦它被定义，r_s就会一直保持，用 □Is_S(x)∧Con_S(x，mem_S)来确保生成结构体变量x的类型和值和结构体类型S保持一 致；如果因为结构体类型S没有定义而导致Sx和S*x不合法，那么在当前状态下r_s为false，并且系统变量healthy设置为’n’。

如图3所示，给出一个链表逆置的例子，示例代码如下：

struct node{int data and node*nexts}；

Frame(s1，s2，s3，p，q，r)and(

//Variable initialization

Node s1，s2，s3and skip；

//Build the linked list

s1.data：＝10；s1.nexts：＝&s2；

s2.data：＝20；s2.nexts：＝&s3；

s3.data：＝30；s3.nexts：＝NULL；

//Pointer initialization

Node*p，*q，*r and skip；

P：＝&s1；q：＝NULL；

//In-place reverse the linked list

While(P！＝NULL)

{r：＝p-＞nexts；p-＞nexts：＝q；q：＝p；p：＝r})

需要说明的是，所述步骤5中对结构体指针类型的赋值操作步骤如下：

对于赋值操作t＝&x的执行，流程如下：

步骤5.1.1，查找符号表，查看变量x是否存在，如果存在，执行步骤5.1.2， 否则执行步骤5.1.5；

步骤5.1.2，查找符号表，查看t是否为结构体指针类型，如果是，执行步 骤5.1.3，否则执行步骤5.1.5；

步骤5.1.3，判断&x的类型和结构体指针t类型是否相等，如果是，执行步 骤5.1.4，否则执行步骤5.1.5；

步骤5.1.4，执行操作t＝&x；

步骤5.1.5，I[t]≠I[&x]，向用户提示t＝&x不满足。

对于赋值操作x＝*t的执行，流程如下：

步骤5.2.1，查找符号表，看变量x是否存在，如果存在，执行步骤5.2.2， 否则执行步骤5.2.5；

步骤5.2.2，在符号表中查找t，首先看t是否是一个结构体指针类型，如 果是，然后再看*t的取值是否为数据域中的一个常量，如果是，执行步骤5.2.3， 否则执行步骤5.2.5；

步骤5.2.3，对变量x的取值进行判断，如果变量x的取值为nil时，将*t 的取值赋给x，使得x＝*t等式满足，赋值操作执行成功，否则执行步骤5.2.4；

步骤5.2.4，如果x的取值不是nil，判断x的取值是否等于*t的取值，如果 相等，那么等式满足，赋值操作执行成功，赋值操作流程结束，如果取值不相 等，执行步骤5.2.5；

步骤5.2.5，I[x]≠I[*t]，向用户提示x＝*t不满足。

需要说明的是，所述步骤5中的结构体类型的赋值操作步骤如下：

对于赋值操作x＝S.a的执行，流程如下：

步骤5.3.1，查找符号表，看变量x是否存在，如果存在，执行步骤5.3.2， 否则执行步骤5.3.5；

步骤5.3.2，查找符号表，检查变量S是否为结构体类型，如果是，执行步 骤5.3.3，否则执行步骤5.3.5；

步骤5.3.3，遍历结构体S的存储链表，找出成员a所在项，如果查找成功， 执行步骤5.3.4，否则执行步骤5.3.5；

步骤5.3.4，执行操作x＝S.a；

步骤5.3.5，I[x]≠I[S.a]，向用户提示x＝S.a不满足。

对于赋值操作x＝t-＞a的执行，流程如下：

步骤5.4.1，查找符号表，看变量x是否存在，如果存在，执行步骤5.4.2， 否则执行步骤5.4.6；

步骤5.4.2，查找符号表，看t是否为结构体指针类型，如果是，执行步骤 5.4.3，否则执行步骤5.4.6；

步骤5.4.3，查找符号表，看t所指的变量是都为结构体类型，如果是，执 行步骤5.4.4，否则执行步骤5.4.6；

步骤5.4.4，遍历t所指的结构体的存储链表，找出成员a所在项，如果查 找成功，执行步骤5.4.5，否则执行步骤5.4.6；

步骤5.4.5，执行操作x＝t-＞a；

步骤5.4.6，I[x]≠I[t-＞a]，向用户提示x＝t-＞a不满足。

本发明的有益效果在于：本发明在MVSL基本数据类型和指针类型的基础上， 扩展结构体以及结构体指针类型，使得MSVL可以运用在包含更加复杂的数据类 型的系统中，对系统进行建模、仿真和验证，也使得MSVL和传统编程语言之间 的差距减小，使得MSVL更加的实用。

附图说明

图1为本发明的系统模块构成示意图；

图2为用指针实现三个整数从大到小排序示例示意图；

图3为链表逆置示例示意图。

具体实施方式

以下将结合附图对本发明作进一步的描述，需要说明的是，本实例以本技 术方案为前提，给出了具体的实施方式，但并不限于本实施例。

如图1所示，MSVL中结构体及结构体指针类型的扩展解释系统及其扩展方 法，所述系统包括如下模块：

结构体类型定义模块：所述结构体类型定义模块包括结构体类型的定义；

结构体变量定义声明模块：所述变量定义声明模块包括所述变量声明命令 以及类型声明定义；

结构体变量存储模块：所述变量存储模块包含有变量类型标记和变量取值， 所述变量类型标记根据变量声明语句记录该变量的类型，变量存储两边的取值 限制在其类型所对应的论域内；

结构体及结构体指针类型赋值操作处理模块：赋值操作的左操作数为变量， 右操作数为表达式并对左操作数进行解释。

基于上述系统的MSVL中结构体以及结构体指针类型的扩展方法，实施步骤 如下：

1、基本数据类型集合用表示，包括：

①原始数据类型：int float char

②列表类型：int<>float<>char<>

③数组类型：int[]float[]char[]

2、由于在类型声明时，定义一个数组需要给定数组长度，比如：int[a]5。 所以修改基本数据类型集合为

int[1]，int[2]，...，float[1]，float[2]，...，char[1]，char[2]，...}

3、基本数据类型论域用表示，

Float[]∪Char∪Char<>∪Char[]

其中，

4、用Is_T定义表示一种数据类型，其中从而可以得到类型声明公式：

5、定义一个解释I[e]来表示变量e类型化的值，其中nil表示 变量还未定义。

例如：I[8]＝(8，int)，I[<′x′，′y′>]＝(<′x′，′y′>，char<>)。

6、对于每一种数据类型，引入指针类型，记作T*，而指针类型的集合用 表示；

7、指针类型的解释需要一个合适的地址模型。一种可能性就是把地址模型 当作是位置到值得映射，这种情况下，用”&x”符号来取得变量x的地址。但是 这种方法不够抽象，因为这依赖一些例如具体内存地址的实现细节。为了使得 实现更加灵活，可以把指针t解释为(x，int)，表示指针t指向变量x，而*t 解释为x。

8、定义指针类型的论域其中，代表所有变量名的集 合，NULL是一个空指针。

9、如果t为空指针，t的解释I[t]＝(NULL，T*)，否则I[t]＝(x，T*)。

10、指针的基本操作是引用(&)和解引用(*)。定义如下：

11、空指针在程序中是非常有用的，所以MSVL中，也允许NULL_T*在程序中 出现；其中因为每一个表达式要有确定的类型，所以下标T*一般情况 不能省略。只有在省略后不引起歧义的情况下才可以省略；

例如：t₁和t₂分别代表int*和char*，那么公式t₁＝NULL_int*∧t₂＝NULL_char*可以简 写为t₁＝NULL∧t₂＝NULL，这样我们不可能误以为是t₁＝t₂。

12、在基本数据类型，已经定义用Is_T(·)来表示一种T类型。现在把指针类型 扩展进去。

13、把指针类型扩展进去；对于每一个指针类型，定义如下：

并且

其中，是bool类型，上式解释为，如果变量v是T类型，则为true，否 则为false；

14、如下定义指针类型变量的声明：

其中，

15、在指针类型的基础上，在MSVL中引入结构体(struct)类型，用S表 示，表示一个可数的结构体类型集合，即对每一种结构体类型，用S*来 表示结构体S的指针类型，因此，所述结构体中指针类型的集合可以表示为

用来表示基本数据类型、指针类型、结构体类型和与之 相关联的指针类型的集合。这样，就可以如下定义结构体：

struct S{T₁a₁，...，T_ka_k}

其中(\表示除去)；

这样就定义了一个结构体S，它的每一个成员a_k分别对应类型T_k。

为了简化这个理论，不允许结构体嵌套，但是允许一个结构体成员的指针 指向另一个结构体类型。这样，就可以容易地定义链表、树和图等复杂数据类 型。

16、一旦定义好一个结构体类型S，就可以用Sx来声明一个新的结构体类型 变量。所以，x就拥有的所有成员类型，可以用x.a来表示的每一个成员。同样还 可以定义一个结构体指针类型S*t，用t-＞a来指向结构体类型的成员a。

17、结构体指针类型论域：和其他类型指针一样，定义一个结构体指针类 型如果为空指针，把t解释为(NULL，S*)。否则，把t解释为(x，S*)。

综上所述，结构体指针类型的论域可以如下定义：

18、结构体论域：结构体类型定义为struct S{T₁a₁，...，T_ka_k}，对于每一个类型的 变量x把它解释为其中所以，对于x的论域 其实就是它每一个成员变量论域的集合，其中涉及到基本数据类型域指针类 型域或者结构体指针类型域

综上所述，结构体类型的论域可以如下定义：

可以得出为一个嵌套的二元组。其中，FPF(E₁，E₂)表示从集合E₁到集合E₂所 有的有限偏函数。如下定义FPF：

其中，E是有限的，并且如果(u，v)，(u，v′)∈E，那么v＝v′，即u和v是一 一对应的。

19、结构体的操作：结构体的基本操作是结构体成员的存取。对每一个成 贝a表示结构体成员的名字。定义“.a”来进行成员的存取操作。假定e是一 个结构体类型，而a是它的一个成员，那么e.a就返回成员a。

所以，就有了如下定义：

20、之前在指针类型部分定义过一般指针的引用和解引用操作，对于结构 体指针类型同样适用。假定t是一个指向结构体类型a结体指针类型，用t-＞a就 可以返回a。

所以，就有了如下定义：

21、和基本数据类型指针一样，在程序中我们也允许结构体指针类型为空， 表示为NULL_T*，其中

结合之前的基本数据类型指针，我们可以把NULL_T*解释为(NULL，T*)，其中， 同样的，当下标T*省略不会引起歧义时可以省略。

22、之前已经定义过用Is_T(·)表示一种T类型。对于基本数据类型和指针类型 有现在对其进行扩展，把结构体类型引入就得到并且对于每一 个都有

并且

23、由于结构体类型的复杂性，用逻辑公式来进行结构体的形式化定义和 变量声明并不是一件容易的事，所以不得不考虑一些细节问题：

首先，要考虑结构体类型定义不合法的可能性。用下面的定义：

来声明结构体S的成员。这种情况下，规定如果S_i(1≤i≤m)的定义不迟于结 构体S的定义，结构体S的定义就是合法的。否则，就不合法。

例如：在程序struct S₁{int a}∧○(struct S₂{S₁*a₂})中，S₁在S₂之前定义，所以S₂是合 法的。另外一个程序struct S₁{S₂*a}∧struct S₂{S₁*a₂}中，因为S₁和S₂是同时定义的， 所以也是合法的。

对于如何处理不合法的结构体类型定义，一种自然的想法就是让包含有不 合法结构体类型定义的不健康程序不可满足，也就是说该程序不合法。但是， 这种方法不可行。对于程序struct S₂{S₁*a₂}来说，它本身就是不健康的程序，也就 是说如果struct S₂{S₁*a₂}是不满足的，那么struct S₁{S₂*a₁}∧struct S₂{S₁*a₂}也就是不满 足的，但是实际又是满足的，这就产生了矛盾。为了解决这个矛盾，引入一个 系统变量字符类型变量healthy，healthy变量只有两个值，y(yes)和n(no)， 默认值为y，只有在一些坏情况下，healthy值设置为n。我们不允许在程序中 出现一个显示的系统变量，所以我们要求程序员不能修改healthy变量的值。 为了处理这些不健康的程序，我们充分利用系统变量healthy重新规范地定义 结构体如下：

其中

24、对于每一个结构体类型S，我们引入r_s表示它是否定义过。S一旦定义， r_s就一直保持是true，只有S未定义前是false。这是因为我们遵循MSVL极小 模型语义的规则。在极小模型语义中，一个命题独立于其他命题可以为真，也 可以为假时，它被解释为假；如果struct S{T₁a₁，...，T_ka_k]是不合法的，那么在当前状态为假，并且把healthy变量的值设置为’n’。我们称一个区间σ是健康 的，当且定当区间对σ的每一个状态都有：s[healthy]＝(′y′，char)。这样，一个包含 不合法结构体类型定义的程序没有一个健康的极小模型。

25、为了定义系统变量healthy，我们假定每一个程序p开始时，都用一个 特别的公式initsys(p)来指定系统变量，整个程序就可以写成initsys(p)∧p。 init sys(p)定义如下：

其中，initsys(p)表示p的初始化。r_healthy表示之前没有出现过，默认为′y′。

根据极小模型语义，没有被赋值时为false；那么，从上式就可以看出 healthy变量默认值是’y’，只有在出现一些例如不合法结构体类型定义的坏情况 下值才被改为’n’。

26、我们需要依据结构体成员以及他们的类型确保结构体变量和结构体类 型定义的一致性。

在结构体变量x拥有结构体类型S同样的成员以及类型时，我们认为结构体 变量x和结构体类型S是一致的，也就是说：

当结构体被定义为struct S{T₁a₁，...，T_ka_k]，x被解释为其中

27、为了确保一个结构体变量和它成员的一致性，在结构体变量定义时记 录它每个成员的信息，然后用来限制每一个结构体变量。为此，再度引入一个 系统变量mem_s，定义为：

这样得到一个特殊类型：

其中MEMTYPE是用来记录结构体每个成员的信息。

28、下面给出结构体的最终定义：

其中当k＝0时，常量{(a₁，T₁)，...(a_kT_k)}是空集并且给出initsys(p)的最终规范定义：

其中，S₁，...，S_n都是程序p中出现过的结构体。如果

某个S_i未被定义，则初始化为

29、为了检查结构体变量和定义的一致性，定义一个断言Con_s，用Con_s(x，mem_s) 表示一致；

对于每一个并且{(a₁，T₁)，...(a_kT_k)}∈MEMTYPE，都有：

并且

当且定当有

形式化表示必须区分变量声明的合法与不合法。对于结构体S，如果结构体 类型定义struct S{}不迟于变量声明Sx或者S*，我们就称之为合法的变量声明， 否则，为不合法的。

Sx∧struct S{...}之前我们定义过一个包含不合法的结构体类型定义的程序为 不健康的程序，现在我们将其扩展为，一个包含不合法的结构体类型定义或者 不合法的变量声明的程序，我们称之为不健康的程序。换句话说就是一个健康 的程序要求它结构体类型定义和变量声明都要合法。

和之前不合法的结构体类型定义一样，想要使一个包含不合法变量声明的 程序不可满足，理论上也是不可实行的。为了处理这些不健康程序，结合系统 变量healthy给出更规范的变量声明：

如果一个结构体变量声明Sx是合法的，一旦它被定义，r_s就会一直保持，用 □Is_S(x)∧Con_S(x，mem_S)来确保生成变量x的类型和值和结构体S保持一致；如果因为 结构体S没有定义而导致Sx和S*x不合法，那么在当前状态下r_s为false，并且 系统变量healthy设置为’n’。

综上，得出结论：

1)一个包含不合法结构体类型定义或者不合法变量声明的不健康程序， 没有一个健康的极小模型。

2)一个健康的程序没有一个不健康的极小模型。

30、结构体指针类型的赋值操作步骤如下：

30.1、对于赋值操作的t＝&x执行，流程如下：

步骤1，查找符号表，查看变量x是否存在，如果存在，执行步骤2，否则执 行步骤5；

步骤2，查找符号表，查看t是否为结构体指针类型，如果是，执行步骤3， 否则执行步骤5；

步骤3，判断&x的类型和结构体指针类型t是否相等，如果是，执行步骤4， 否则执行步骤5；

步骤4，执行操作t＝&x；

步骤5，I[x]≠I[*t]，向用户提示t＝&x不满足。

30.2、对于赋值操作x＝*t的执行，流程如下：

步骤1，查找符号表，看变量x是否存在，如果存在，执行步骤2，否则执行 步骤5；

步骤2，在符号表中查找t，首先看t是否是一个结构体指针类型，如果是， 然后再看*t的取值是否为数据域中的一个常量，如果是，执行步骤3，否则执 行步骤5；

步骤3，对变量x的取值进行判断，如果变量x的取值为nil时，将*t的取值 赋给x，使得x＝*t等式满足，赋值操作执行成功，否则执行步骤4；

步骤4，如果x的取值不是nil，判断x的取值是否等于*t的取值，如果相等， 那么等式满足，赋值操作执行成功，赋值操作流程结束，如果取值不相等，执 行步骤5；

步骤5，I[x]≠I[*t]，向用户提示x＝*t不满足。

31、对结构体类型的赋值操作步骤如下：

31.1、对于赋值操作x＝S.a的执行，流程如下：

步骤1，查找符号表，看变量x是否存在，如果存在，执行步骤2，否则执行 步骤5；

步骤2，查找符号表，检查变量S是否为结构体类型，如果是，执行步骤3， 否则执行步骤5；

步骤3，遍历结构体S的存储链表，找出成员a所在项，如果查找成功，执 行步骤4，否则执行步骤5；

步骤4，执行操作x＝S.a；

步骤5，I[x]≠I[S.a]向用户提示x＝S.a不满足。

31.2、对于赋值操作x＝t-＞a的执行，流程如下：

步骤1，查找符号表，看变量x是否存在，如果存在，执行步骤2，否则执行 步骤6；

步骤2，查找符号表，看t是否为结构体指针类型，如果是，执行步骤3， 否则执行步骤6；

步骤3，查找符号表，看t所指的变量是都为结构体类型，如果是，执行步 骤4，否则执行步骤6；

步骤4，遍历t所指的结构体的存储链表，找出成员a所在项，如果查找成 功，执行步骤5，否则执行步骤6；

步骤5，执行操作x＝t-＞a；

步骤6，I[x]≠I[t-＞a]，向用户提示x＝t-＞a不满足。

对于本领域的技术人员来说，可以根据上述的技术方案和构思，给出各种 相应的改变和变形，而所有的这些改变和变形都应该包括在本发明权利要求的 保护范围之内。