一种基于时序逻辑语言MSVL的函数调用方法

摘要

本发明公开了一种基于时序逻辑语言MSVL的函数调用方法，首先判断被调用函数的类型是MSVL函数、有返回值的外部函数还是无返回值的外部函数，根据不同的函数类型对被调用函数进行定义或者修改其定义；然后判断函数调用的位置，根据不同的函数调用位置以及相应的被调用函数类型，以不同的方式进行调用。本发明可以在同一程序中以不同的方式对被调用函数进行解释；并且在MSVL程序中可以调用由C语言和Java语言编写的函数，有利于多种不同编程语言程序的集成，有效降低程序开发的难度，提高代码复用率。

说明书

技术领域

本发明属于计算机系统形式化建模与验证技术领域，主要涉及的 是逻辑程序设计语言的实现，特别是一种基于时序逻辑语言MSVL的 函数调用方法，可用于在MSVL程序中调用其它多种不同语言程序， 有利于代码的复用和集成，简化程序设计。

背景技术

1977年，A.Pnueli将时序逻辑引入到计算机科学领域，主要用 于对实时、并发系统进行建模和验证。经过近40年的研究，时序逻 辑领域已经得到了很大的发展，形成了三大分支：线性时序逻辑 (Linear Temporal Logic)、分支时序逻辑(Branching Temporal  Logic)和区间时序逻辑(Interval Temporal Logic)。

投影时序逻辑(Projection Temporal Logic)是一种区间时序 逻辑，区间的含义为有穷或无穷的状态序列，序列中的状态个数减1 为区间长度，当为无穷状态序列时，区间长度被定义为无穷大，即ω。 PTL以投影操作符(prj)为特色，可用于描述执行在不同粒度区间 上的并发进程的并行执行。

逻辑程序设计语言(MSVL)是投影时序逻辑的一个可执行子集， 可用于对并发、实时系统进行建模(Modeling)、仿真(Simulation) 和验证(Verification)。MSVL包含了大多数命令式程序设计语言(如 C语言)中的常用语句和编程结构，例如赋值语句(：＝)、顺序结构 (；)、分支结构(if-then-else)和循环结构(while)，因此它可以 实现一般命令式程序设计语言能够实现的大多数功能。MSVL中还包 括一些并发类编程结构，如合取(and)，并行(||)和投影(prj)， 其中合取结构P1 and P2表示进程P1和P2并行执行在同样长度的区 间上，且共享区间上的所有状态；并行结构P1||P2表示进程P1和 P2可自行规定各自执行的区间长度，且共享较短区间上的所有状态； 投影结构(P1，...，Pm)prj Q表示进程Pi(i＝1，...，m)顺序执行，由 每个Pi执行区间的端点状态顺序排列构成的一个较粗粒度的投影区 间，或该投影区间的某个前缀，或以该投影区间为前缀的某个区间被 作为进程Q的执行区间。投影结构体现了多个进程之间的并发性和自 治性。另外，由于在时序逻辑程序设计中，变量的值不能自动从当前 状态传递到下一状态，因此MSVL中的框架结构(frame)用于变量值 在相邻状态间的传递。除此，MSVL中还包括异步通信结构(await)， 可用于对分布式系统进行建模和验证。MSVL中的数据类型包括整数 类型，浮点类型，字符类型，字符串类型，指针类型和结构类型。基 于MSVL的类型系统，可以定义函数和谓词。函数是程序设计中一种 十分有用的构建模块，函数可以对数据和操作进行有效封装，对外只 提供一个简单的函数接口，当程序需要执行一个同样的功能时，可以 直接调用写好的函数，而不用重新编写代码，从而提高代码复用率， 简化程序设计，使程序更加简洁精炼，但MSVL中还没有给出函数定 义及调用的实现方法，这一缺陷给MSVL程序设计带来不便，同时导 致MSVL程序冗长，不易理解。

发明内容

针对现有技术的不足，本发明旨在提供一种基于时序逻辑语言 MSVL的函数调用方法，通过该方法，可以在同一程序中以不同的方 式对被调用函数进行解释；并且在MSVL程序中可以调用由C语言和 Java语言编写的函数，有利于多种不同编程语言程序的集成，有效 降低程序开发的难度，提高代码复用率。

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

一种基于时序逻辑语言MSVL的函数调用方法包含如下步骤：

步骤1，判断被调用函数是否为MSVL函数，如果是，定义该函 数；如果不是，判断被调用函数是否为有返回值的外部函数，如果是， 则执行步骤2，如果被调用函数为无返回值的外部函数，则执行步骤 3；

当所述被调用函数为MSVL函数时，根据形式的不同，分四种情 况对该函数进行定义：

1)有参数有返回值，则定义格式如下：

def ine f(in_type x1，...，in_type xn，out_type y1，...，out_type  ym，return_type RV[]){MSVL程序}；

2)有参数无返回值，则定义格式如下：

def ine f(in_type x1，...，in_type xn， out_type y1，...， out_type ym){MSVL程序}；

3)无参数有返回值，则定义格式如下：

def ine f(return_type RV[]){MSVL程序}；

4)无参数无返回值，则定义格式如下：

def ine f(){MSVL程序}；

定义该函数后，定义一个调用该函数的MSVL程序并执行步骤3；

步骤2，修改所述有返回值的外部函数的定义，具体分两种情况 进行修改：

若所述有返回值的外部函数有参数，即原定义为：

return_type f(in_type x1，...，in_type xn，out_type y1，...， out_type ym){C/Java程序}；

则需做以下两点修改：

(1)函数定义的头部改为：

void f(in_type x1，...， in_type xn，out_type y1，...，out_type  ym，return_type RV[])；

(2)函数定义体中的所有“return value”语句被替换为 “RV[0]＝value”；

若所述有返回值的外部函数无参数，即原定义为：

return_type f(){C/Java程序}；

则需做以下两点修改：

(1)函数定义的头部改为：void f(return_type RV[])

(2)函数定义体中的所有“return value”语句被替换为 “RV[0]＝value”；

修改有返回值的外部函数定义后，定义一个调用该函数的MSVL 程序并执行步骤3；

步骤3，规定所有在MSVL表达式中出现的函数调用均属黑盒调 用，其中用关键字ext修饰的为外部函数的黑盒调用，没有ext修饰 的为MSVL函数的黑盒调用；在语句中出现的函数调用没有关键字ext 修饰的为MSVL函数的白盒调用，有ext修饰的为MSVL或外部函数的 黑盒调用，现判断函数调用出现的位置：

若函数调用出现在MSVL表达式中且没有关键字ext修饰，即属 于MSVL函数的黑盒调用，则执行步骤4；若MSVL表达式中的函数调 用有关键字ext修饰，即属于外部函数的黑盒调用，则执行步骤5； 若函数调用以独立语句出现且没有关键字ext修饰，即属于MSVL函 数的白盒调用，则执行步骤6；若函数调用以独立语句出现且有关键 字ext修饰，即属于MSVL函数或外部函数的黑盒调用，则执行步骤 7；

步骤4，求出被调用的MSVL函数实参列表中所有实参变量在调 用程序当前状态下的值，并对定义该函数的MSVL程序初始化，同时 保存原调用程序的执行环境，此时，若定义函数的MSVL程序为简单 结构，执行步骤8，若定义函数的MSVL程序为复杂结构，则该程序 进行递归结构变换，即对程序进行等价变换，将其转换为一个简单结 构程序，然后执行步骤8；

步骤5，求出被调用的外部函数实参列表中所有实参变量在调用 程序当前状态下的值，然后将这些参数值传递给C或Java函数执行， 函数返回值作为外部函数在MSVL表达式中的值；

步骤6，求出被调用的MSVL函数实参列表中所有实参变量在程 序当前状态下的值，此时，若定义函数的MSVL程序为简单结构，执 行步骤9，若定义函数的MSVL程序为复杂结构，则对该程序进行递 归结构变换，转换为简单结构，然后执行步骤9；

步骤7，若被调用函数为MSVL函数，执行步骤4；若为外部函数， 执行步骤5；

步骤8，简单结构在当前状态分为当前状态程序集合和下一状态 程序集合；本步骤具体包含如下步骤：

步骤8.1，在当前状态对简单结构进行一次解释，即执行当前状 态程序集合中的语句，执行效果反映在程序变量的更新和程序结构的 改变上；然后执行步骤8.2；

步骤8.2，判断下一状态程序集合是否为空：如果下一状态程序 集合不为空，则将下一状态程序集合作为新的待执行程序，然后改变 函数程序的时序状态，从当前时序状态跳转到下一时序状态，此时， 若新的待执行程序为简单结构，则返回执行步骤8.1，若新的待执行 程序为复杂结构，则对该程序进行递归结构变换，转换为一个简单结 构，然后返回执行步骤8.1；如果下一状态程序集合为空，则恢复调 用程序的执行环境，然后被调用函数将控制权交还给调用程序，函数 调用的计算过程结束，此时被调用函数的返回值已通过变量RV[0]传 递给了调用程序，若函数的执行区间长度大于0，则将函数执行的终 止状态作为调用程序当前状态的下一状态，并将调用程序从当前状态 跳转到下一时序状态，然后调用程序继续执行，若函数的执行区间等 于0，即状态函数，则调用程序从当前状态继续执行；

步骤9，简单结构在当前状态分为当前状态程序集合和下一状态 程序集合；本步骤具体包含如下步骤：

步骤9.1，在当前状态对简单结构进行一次解释，即执行当前状 态程序集合中的语句，执行效果反映在程序变量的更新和程序结构的 改变上；然后执行步骤9.2；

步骤9.2，判断下一状态程序集合是否为空：如果下一状态程序 集合不为空，则将下一状态程序集合作为新的待执行程序，然后改变 函数程序的时序状态，从当前时序状态跳转到下一时序状态，此时， 若新的待执行程序为简单结构，则返回执行步骤9.1，若新的待执行 程序为复杂结构，则对该程序进行递归结构变换，转换为一个简单结 构，然后返回执行步骤9.1；如果下一状态程序集合为空，则恢复调 用程序的执行步骤，并把函数调用产生的状态序列统计到调用函数的 执行区间，然后被调用函数将控制权交还给调用程序，此时函数调用 的计算过程结束，调用程序则从被调用函数执行的结束状态继续执行。

需要说明的是，函数黑盒调用的语法定义如下：

MSVL函数的黑盒调用语法：ext MSVL函数名(实参列表，RV)；

外部函数的黑盒调用语法：ext外部函数名(实参列表，RV)。

需要说明的是，步骤3中，所述的MSVL表达式的语法定义为：

对单个带类型的常量：a，b，c，...∈D是基本表达式，其中基本 表达式可含下标；

对单个带类型的静态变量和动态变量：u，v，x，y，z，...∈V是 基本表达式，其中基本表达式可含下标；

若x是变量，则Ox和Θx是表达式；

若op是MSVL中的n元操作符(n＞0)，e1，...，en是n个类型与 op的参数类型相兼容的表达式，则op(e1，...，en)是表达式；

若h是n元MSVL状态函数(n＞0)，e1，...，en是n个类型与h参 数类型相兼容的表达式，则h(e1，...，en，RV)是表达式；

若f是n元MSVL时序函数(n＞0)，e1，...，en是n个类型与f参 数类型相兼容的表达式，则f(e1，...，en，RV)是表达式；

若g是n元外部函数(n＞0)，e1，...，en是n个类型与g参数类 型相兼容的表达式，则ext g(e1，...，en，RV)是表达式。

需要进一步说明的是，步骤3中，所述的MSVL表达式e的语义 解释为MSVL表达式e在给定状态区间的当前状态处的值，它是通过 解释I＝(σ，i，k，j)来定义的：

I对带类型常量的解释为该常量的值；

I对静态变量的解释为该变量在该状态区间的首状态处的值；

I对动态变量的解释为该变量在该状态区间的当前状态处的值；

I对Ox的解释为：若k＜j，则结果为以S_k+1为当前状态的新解释 (σ，i，k+1，j)对x的解释；否则，解释结果为nil；

I对Θx的解释为：若i＜k，则结果为以S_k-1为当前状态的新解释 (σ，i，k-1，j)对x的解释；否则，解释结果为nil；

I对op(e1，...，en)的解释为：将操作op应用于表达式e1，......，en 在I的解释下所得的结果；

I对h(e1，...，en，RV)的解释为：以表达式e1，......，en在I下的 解释对状态函数h的实参变量初始化后，程序执行结束时RV[0]的值；

I对f(e1，...，en，RV)的解释为：以表达式e1，......，en在I下的 解释对时序函数f的实参变量初始化后，程序执行结束时RV[0]的值；

I对ext g(e1，...，en，RV)的解释为：以表达式e1，......，en在I 下的解释对外部函数g的实参变量初始化后，程序执行结束时RV[0] 的值。

需要再进一步说明的是，步骤3中，所述的黑盒调用的语义定义 为解释I＝(σ，i，k，j)与MSVL函数的外部调用语句之间的可满足 性关系：

解释I＝(σ，i，k，j)满足ext g(e1，...，en，z1，...，zm，RV)当 且仅当j＝k+1，并且存在一个以S_k为首状态S_j为末状态的区间为后缀， 以σ_(0..k)为前缀，以S_k为当前状态的解释满足由外部调用产生的投影 公式Q，其中：

e1，...，en是函数g的输入实参，可以为表达式；

z1，...，zm是函数g的输出实参，必须为变量，与函数定义中的 形参y1，...，ym对应；

本发明的有益效果在于：本发明实现了能够在同一程序中以不同 的方式对被调用函数进行解释，并且在MSVL程序中可以调用由C语 言和Java语言编写的函数，有利于多种不同编程语言程序的集成， 有效降低程序开发的难度，提高代码复用率。

附图说明

图1为本发明实施的总流程图。

具体实施方式

以下将结合附图对本发明作进一步的描述，需要说明的是，本实 施例以本技术方案为前提，给出详细的实施方式和操作过程，但本发 明的保护范围并不限于本实施例。

如图1所示，一种基于时序逻辑语言MSVL的函数调用方法包含 如下步骤：

步骤1，判断被调用函数是否为MSVL函数，如果是，定义该函 数；如果不是，判断被调用函数是否为有返回值的外部函数，如果是， 则执行步骤2，如果被调用函数为无返回值的外部函数，则执行步骤 3；

当所述被调用函数为MSVL函数时，根据形式的不同，分四种情 况对该函数进行定义：

1)有参数有返回值，则定义格式如下：

def ine f(in_type x1，...，in_type xn，out_type y1，...，out_type  ym，return_type RV[]){MSVL程序}；

2)有参数无返回值，则定义格式如下：

def ine f(in_type x1，...，in_type xn，out_type y1，...， out_type ym){MSVL程序}；

3)无参数有返回值，则定义格式如下：

def ine f(return_type RV[]){MSVL程序}；

4)无参数无返回值，则定义格式如下：

def ine f(){MSVL程序}；

定义该函数后，定义一个调用该函数的MSVL程序并执行步骤3；

步骤2，修改所述有返回值的外部函数的定义，具体分两种情况 进行修改：

若所述有返回值的外部函数有参数，即原定义为：

return_type f(in_type x1，...，in_type xn，out_type y1，...， out_type ym){C/Java程序}；

则需做以下两点修改：

(1)函数定义的头部改为：

void f(in_type x1，...， in_type xn，out_type y1，...，out_type  ym，return_type RV[])；

(2)函数定义体中的所有“return value”语句被替换为 “RV[0]＝value”；

若所述有返回值的外部函数无参数，即原定义为：

return_type f(){C/Java程序}；

则需做以下两点修改：

(1)函数定义的头部改为：void f(return_type RV[])

(2)函数定义体中的所有“return value”语句被替换为 “RV[0]＝value”；

修改有返回值的外部函数定义后，定义一个调用该函数的MSVL 程序并执行步骤3；

步骤3，本发明对函数的解释采用两种方式：黑盒调用和白盒调 用。黑盒调用，即为调用程序只关心函数执行的结果不关心函数执行 的中间过程，即函数执行的中间状态对于调用程序不可见；而白盒调 用，即为调用程序不仅关心函数执行的结果，还关心函数执行的中间 过程，即函数执行的中间状态对调用程序均可见。

规定所有在MSVL表达式中出现的函数调用均属黑盒调用，其中 用关键字ext修饰的为外部函数的黑盒调用，没有ext修饰的为MSVL 函数的黑盒调用；在独立语句中出现的函数调用没有关键字ext修饰 的为MSVL函数的白盒调用，有ext修饰的为MSVL或外部函数的黑盒 调用；

现判断函数调用出现的位置：

若函数调用出现在MSVL表达式中且没有关键字ext修饰，即属 于MSVL函数的黑盒调用，则执行步骤4；若MSVL表达式中的函数调 用有关键字ext修饰，即属于外部函数的黑盒调用，则执行步骤5； 若函数调用以独立语句出现且没有关键字ext修饰，即属于MSVL函 数的白盒调用，则执行步骤6；若函数调用以独立语句出现且有关键 字ext修饰，即属于MSVL函数或外部函数的黑盒调用，则执行步骤 7；

函数黑盒调用的语法定义如下：

MSVL函数的黑盒调用语法：ext MSVL函数名(实参列表，RV)；

外部函数的黑盒调用语法：ext外部函数名(实参列表，RV)。

所述的MSVL表达式的语法定义如下：

对单个带类型的常量：a，b，c，...∈D是基本表达式，其中基本 表达式可含下标；

对单个带类型的静态变量和动态变量：u，v，x，y，z，...∈V是 基本表达式，其中基本表达式可含下标；

若x是变量，则Ox和Θx是表达式；

若op是MSVL中的n元操作符(n＞0)，e1，...，en是n个类型与 op的参数类型相兼容的表达式，则op(e1，...，en)是表达式；

若h是n元MSVL状态函数(n＞0)，e1，...，en是n个类型与h参 数类型相兼容的表达式，则h(e1，...，en，RV)是表达式；

若f是n元MSVL时序函数(n＞0)，e1，...，en是n个类型与f参 数类型相兼容的表达式，则f(e1，...，en，RV)是表达式；

若g是n元外部函数(n＞0)，e1，...，en是n个类型与g参数类 型相兼容的表达式，则ext g(e1，...，en，RV)是表达式。

MSVL包含的操作符如表1所示：

表1

所述的MSVL表达式e的语义解释为MSVL表达式e在给定状态区 间的当前状态处的值，它是通过解释I＝(σ，i，k，j)来定义的：

I对带类型常量的解释为该常量的值；

I对静态变量的解释为该变量在该状态区间的首状态处的值；

I对动态变量的解释为该变量在该状态区间的当前状态处的值；

I对Ox的解释为：若k＜j，则结果为以S_k+1为当前状态的新解释 (σ，i，k+1，j)对x的解释；否则，解释结果为nil；

I对Θx的解释为：若i＜k，则结果为以S_k-1为当前状态的新解释 (σ，i，k-1，j)对x的解释；否则，解释结果为nil；

I对op(e1，...，en)的解释为：将操作op应用于表达式e1，......，en 在I的解释下所得的结果；

I对h(e1，...，en，RV)的解释为：以表达式e1，......，en在I下的 解释对状态函数h的实参变量初始化后，程序执行结束时RV[0]的值；

I对f(e1，...，en，RV)的解释为：以表达式e1，......，en在I下的 解释对时序函数f的实参变量初始化后，程序执行结束时RV[0]的值；

I对ext g(e1，...，en，RV)的解释为：以表达式e1，......，en在I 下的解释对外部函数g的实参变量初始化后，程序执行结束时RV[0] 的值。

在此基础上，黑盒调用的语义定义为解释I＝(σ，i，k，j)与MSVL 函数的外部调用语句之间的可满足性关系：

解释I＝(σ，i，k，j)满足ext g(e1，...，en，z1，...，zm，RV)当 且仅当j＝k+1，并且存在一个以S_k为首状态S_j为末状态的区间为后缀， 以σ_(0..k)为前缀，以S_k为当前状态的解释满足由外部调用产生的投影 公式Q，其中：

e1，...，en是函数g的输入实参，可以为表达式；

z1，...，zm是函数g的输出实参，必须为变量，与函数定义中的 形参y1，...，ym对应；

步骤4，求出被调用的MSVL函数实参列表中所有实参变量在调 用程序当前状态下的值，并对定义该函数的MSVL程序初始化，同时 保存原调用程序的执行环境，此时，若定义函数的MSVL程序为简单 结构，执行步骤8，若定义函数的MSVL程序为复杂结构，则该程序 进行递归结构变换，即对程序进行等价变换，将其转换为一个简单结 构程序，然后执行步骤8；

步骤5，求出被调用的外部函数实参列表中所有实参变量在调用 程序当前状态下的值，然后将这些参数值传递给C或Java函数执行， 函数返回值作为外部函数在MSVL表达式中的值；

步骤6，求出被调用的MSVL函数实参列表中所有实参变量在调 用程序当前状态下的值，此时，若定义函数的MSVL程序为简单结构， 执行步骤9；若定义函数的MSVL程序为复杂结构，则对该程序进行 递归结构变换，转换为简单结构，然后执行步骤9；

步骤7，若被调用函数为MSVL函数，执行步骤4；若为外部函数， 执行步骤5；

步骤8，简单结构在当前状态分为当前状态程序集合和下一状态 程序集合；本步骤具体包含如下步骤：

步骤8.1，在当前状态对简单结构进行一次解释，即执行当前状 态程序集合中的语句，执行效果反映在程序变量的更新和程序结构的 改变上；然后执行步骤8.2；

步骤8.2，判断下一状态程序集合是否为空：如果下一状态程序 集合不为空，则将下一状态程序集合作为新的待执行程序，然后改变 函数程序的时序状态，从当前时序状态跳转到下一时序状态，此时， 若新的待执行程序为简单结构，则返回执行步骤8.1，若新的待执行 程序为复杂结构，则对该程序进行递归结构变换，转换为一个简单结 构，然后返回执行步骤8.1；如果下一状态程序集合为空，则恢复调 用程序的执行环境，然后被调用函数将控制权交还给调用程序，函数 调用的计算过程结束，此时被调用函数的返回值已通过变量RV[0]传 递给了调用程序，若函数的执行区间长度大于0，则将函数执行的终 止状态作为调用程序当前状态的下一状态，并将调用程序从当前状态 跳转到下一时序状态，然后调用程序继续执行，若函数的执行区间等 于0，即状态函数，则调用程序从当前状态继续执行；

步骤9，简单结构在当前状态分为当前状态程序集合和下一状态 程序集合；本步骤具体包含如下步骤：

步骤9.1，在当前状态对简单结构进行一次解释，即执行当前状 态程序集合中的语句，执行效果反映在程序变量的更新和程序结构的 改变上；然后执行步骤9.2；

步骤9.2，判断下一状态程序集合是否为空：如果下一状态程序 集合不为空，则将下一状态程序集合作为新的待执行程序，然后改变 函数程序的时序状态，从当前时序状态跳转到下一时序状态，此时， 若新的待执行程序为简单结构，则返回执行步骤9.1，若新的待执行 程序为复杂结构，则对该程序进行递归结构变换，转换为一个简单结 构，然后返回执行步骤9.1；如果下一状态程序集合为空，则恢复调 用程序的执行步骤，并把函数调用产生的状态序列统计到调用函数的 执行区间，然后被调用函数将控制权交还给调用程序，此时函数调用 的计算过程结束，调用程序则从被调用函数执行的结束状态继续执行。

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