2014, Vol. 25
Tabular表达式是一种采用表格化结构来组织关系或函数的形式化描述工具[1],它遵循分而治之的原则,对复杂的数学表达式进行分解和简化,在保持定义严谨性的同时,提高了定义的可读性.由于Tabular表达式的准确性和严谨性,它可以用来定义软件开发中的需求文档和技术文档,使得设计者和维护人员可以直观地阅读开发文档中的各项内容.
20世纪70年代末,Parnas等人在为A-7E战斗机设计机载系统时,提出了采用表格的形式描述需求的方法,这就是Tabular表达式的雏形[2, 3, 4].此后,Parnas教授对Tabular表达式进行了深入的研究,发表了一系列的论文,分别在软件安全开发[5, 6]、软件文档的合理性描述[7, 8, 9]等方面阐述了Tabular表达式对软件开发所产生的积极影响.基于Parnas教授的研究成果,先后有很多学者利用Tabular表达式对软件开发过程中存在的问题进行了研究.Degiovanni等人提出了一种自动化的软件测试用例生成方法,基于Tabular表达式需求描述规范生成复杂软件系统的测试用例[10];Feng等人提出了一种软件故障定位方法,利用Tabular表达式追踪故障的产生过
程[11];Herrmannsdörfer等人提出了5种利用Tabular表达式描述有限自动机的方法,并对这些描述方法在软件开发中的价值进行了评估[12];Peters等人开发了一个软件集成开发环境工具,利用Tabular表达式描述软件的需求,并对软件的设计进行测试与验证[13].这些研究表明:Tabular表达式可以有效地解决软件开发过程中软件文档描述不准确和难理解两大难题,保障软件的准确开发.
Tabular表达式最初只包含10种表,各个表的语义解释需要基于函数或者关系的联合单独定义,Janicki对Parnas定义的一部分表给出了统一的形式模型,并采用关系语义对表类型进行了解释[14, 15],但是该模型不能定义向量表和函数表.Abraham指出了Janicki模型的局限性,对该模型进行了扩展,并开发了Tabular表达式求值代码的自动生成工具[16].Kahi为Tabular表达式建立了基于复合形式的语法和语义,其通过增加标题操作和连接操作从一个网格逐步构造Tabular表达式,利用表折叠函数从如何求值的角度定义Tabular表达式的语
义[17].以上这些模型形式语义的定义都依赖于一种特定的物理表示结构,要求将Tabular表达式表示成一个由主网格和若干标题网格组成的多维矩形结构,并要求主网格的索引集是其他标题网格索引集合的笛卡尔乘积.为了打破这一局限,增强Tabular表达式的适用性,parnas教授和金英教授提出了一种Tabular表达式的通用模
型[18],并从如何求值的角度给出了该通用模型的语义.在该模型中,不需要再对网格进行区分,索引集合也不再仅局限于整数集合.
通用模型增强了Tabular表达式的描述能力,同时也增加了Tabular表达式语义描述的难度.Tabular通用模型用类型概念,从表达式组成和求值方案两个角度去刻画一类Tabular表达式所共有的特征,如网格个数、索引集合、网格包含的表达式类型、表达式的计算过程以及在求值过程中使用的一些辅助函数等.但是由于通用模型可以定义无穷种类型,表达式类型无法一一穷举,因而定义Tabular表达式如何求值无法完整地刻画Tabular表达式通用模型的语义,存在着一定的局限性.为克服这一不足,本文以定义Tabular表达式形式文法的形式给出了Tabular表达式通用模型的相关论域,并给出了各语法成分到论域上的语义映射,首次从指称语义的角度完善了Tabular表达式的形式语义,为Tabular表达式应用的进一步推广和相关模型验证工具的开发奠定了良好的基础.
本文第1节介绍Tabular表达式通用模型的形式文法和一些基本定义.第2节阐述Tabular表达式通用模型指称语义的描述方法.第3节和第4节分别就传统类型和新定义类型中一些Tabular表达式的指称语义进行描述,说明本文方法的有效性.第5节对本文的方法和一些相关进行了比较.最后是本文工作的总结.
1 基本定义Tabular表达式通用模型是目前为止扩展性最好的模型.本文针对该模型从Tabular表达式语法单元的功能的角度给出Tabular表达式的形式语义,该模型的形式化文法定义如下:
· Tabular::=Indexes®Grids
· Indexes::={Index}
· Index::=integer|identifier|IndexxIndex
· Grids::={Grid}
· Grid::=Indexes®Expresses
· Expresses::={Express}
· Express::=Tabular|Scalar_express
· Scalar_express::=variable|constant|R(Scalar_express,Scalar_express)
其中,integer表示整数,identifier表示表示符,variable表示变量,constant表示常量,Scalar_express表示标量表达式,R表示标量表达式间的二元关系.Tabular表达式的本质是一个索引化的网格集合,而网格的本质是一个索引化的表达式集合.
定义1. 设存在n个逻辑公式F1,F2,…,Fn和指令集Instruct_Set,给定指派assign,若assign满足所有Fi(1≤i≤n),则执行指令集Instruct_Set,称F1®F2®…®Fn®Instruct_Set为一个指引,n为指引的维度,将n维指引记做FI(n).
指引的物理意义是指令集被执行的前提,是满足n个条件,只有n个条件全被满足时,该指令集才能被执行,当n=0时,指令集可以永远被执行.这里的指令集与程序语言中指令集有所区别,指令可以是一种操作,也可以是一种判断结果,在不同情况下可以被赋予不同的意义,后文将在Tabular语义情景环境下对指令的功能指代物进行讨论.
定义2. 已知S为逻辑公式的集合,"F1,F2ÎS,若有F1ÙF2=Æ,则称S是互斥的.
定义3. 已知S为逻辑公式的集合,设S={F1,F2,…,Fn},若F1ÚF2Ú…ÚFn=1,则称S是完备的.
互斥公式集合S可以用来形容函数的定义域,函数的参数作为公式中的变量,一组参数最多只能满足S中一个逻辑公式.由于函数可能是部分函数,因而存在一组参数不满足S中任何公式的情况.若用一个互斥且完备的公式集合S来形容函数的定义域,则该函数为完全函数,一组参数能且只能满足S中的一个公式.
定义4. 已知S为包含n个逻辑公式的集合,设S={F1,F2,…,Fn},给定一个公式的解释I,P为S中在解释I下为真的逻辑公式的集合,称S®P为集合S的一个指派,记做assign(S).
当S为互斥集合时,P中最多只有一个逻辑公式;当S为互斥且完备集合时,P中有且只有一个逻辑公式.
定义5. 已知E为标量表达式,称E®Value为E的一个指派,记做assign(E).
互斥集合指派的物理意义是:给定参数的赋值,使得互斥集合中的一个公式为真,其他的公式为假,进而执行相应的指令集;表达式指派的意义是:给定参数的赋值,求取标量表达式的计算结果.
定义6. 已知G1和G2是Tabular表达式中的两个Grid,若G1中的任何一个表达式都可以在G2中找到,则称G1是G2的子网格.
网格G实际上相当于一个表达式的集合,因而任何该集合子集构成的网格都是G的子网格.
2Tabular表达式的语义本节将对Tabular表达式中各语法单位的功能进行分析,进而给出各语法单位的语义指代物和相应的语义指派方程.
Tabular表达式中各语法单位的功能如下:
· Tabular:一组说明规范,明确不同条件下应对哪些事物进行处理;
· Index:对规范和事物进行分类;
· Grid:一项说明规范,明确不同事物的处理条件;
· Scalar_express:一项事物的处理过程;
· Variable:一个变量;
· Constant:一个常量.
通过上面的说明,可以给出Tabular表达式中各语法单位所对应的语义域,见表 1.
|
Table 1 Semantic domain of tabular expressions 表 1 Tabular表达式的语义域 |
指引可以表示一件事物的说明规范,因而可以用n维指引集{FI(n)}表示Tabular表达式的指称语义,Tabular表达式的语义本质就是根据n个辅助主题来决定怎样处理一组事物;Tabular表达式中的每一个Grid都对事物的最终处理有影响,但给定一个Grid的指派并不能完全决定事物如何被处理,只能降低影响事物因素的数目,因而一个Grid g的指称语义为通过给定一个指派assign(g)将n维指引集{FI(n)}映射为一个维度较小的m维指引集{FI(m),大多数情况下,m=n-1,当 n=0时,assign(g)将一组指令集映射为操作结果;Scalar_express的指称语义为根据当前环境的指派情况给出一件事物的处理结果.Variable和Constant都是特殊的Scalar_ express,其语义本质与Scalar_express相同;Index在Tabular表达式中起到索引的作用,其指称语义就是网格或者表达式的索引标签.
Grid是索引化的表达式集合,由于表达式包含标量表达式和Tabular表达式两种,因而表达式的计算结果可以是一个值,也可以是指引集,只是指引集的维度要小于当前指引集的维度.值得注意的是,这里,Value的意义并不仅仅局限于数学上的数值,而是一件事物的处理结果,可以是数值或状态,也可以是一个决定,具体取值取决于事物本身的属性.
根据上文的分析可知,Tabular的指称语义是一个指引集,在这个情景环境下,指引中的指令相当于Tabular表达式中的express,因而指引中的指令可以是标量表达式,也可以是Tabular表达式.标量表达式由变量、常量和变量表达式间的二元关系构成,由于任何一种运算的本质都是将算子作用在变量或常量上,算子就是量纲之间的二元关系.因而,本文用逻辑公式来描述标量表达式,当两个量纲x和y具有关系R时,逻辑公式R(x,y)返回为真值,否则为假值.
若设指引集S包含n个指引,第i(1≤i≤n)个指引FIi=Fi1®Fi2®…®Fim®Instruct_Seti,则经过如下变换可以将S转换为等价的逻辑公式F:
1) 将第i(1≤i≤n)个指引FIi转换Fi=ØFi1ÚØFi2Ú…ÚØFimÚInstruct_Seti;
2) F=F1ÚF2Ú…ÚFn.
由于每个指引FIi的指令集是标量表达式或者Tabular表达式,并且可以变换为相应的逻辑公式,因而指引集可以转换为等价的逻辑公式.也就是说,express可以转换为等价的逻辑公式. Grid是索引化的表达式集合,因而Grid的语义本质是逻辑公式的集合.
语义指派函数将语法域中的每个语法单元映射为相应的语义指代物,Tabular表达式各语法单元语义指派函数的函数空间如下:
· KT:Tabular®Account(n)
· KG:Grid®[assign(g)xAccount(n)®Account(m)]+[assign(g)xAccount(0)®{Value}](n>m)
· KE:Express®[{assign(g)+assign(E)}xAccount(n)®Account(m)+Value](n>m)
· KSE:Scalar_express®[{assign(E)}®Value]
· KI:Index®[Tabular®Grid]+[Grid®Express]
· KV:Variable®[{assign(s)}®Value]
· KC:Constant®Constant
由于变量本身也属于标量表达式,因而它们的语义指派函数具有相同的函数空间;常量虽然也属于标量表达式,但由于常量的值和指派环境无关,只与自身有关,因而常量的语义指代物是自身的值.在对维度为0的指引集做指派时,相当于对Grid中的标量表达式做指派,此时,assign(g)的作用相当于assign(E)的集合,如果Grid中只有一个标量表达式,则assign(g)与assign(E)的作用相同.
我们曾在文献[18]中从如何求值的角度研究了Tabular表达式的语义,用通用函数eval解释Tabular表达式的语义,eval对传统的表达式计算进行了扩充,其定义域是传统表达式和所有Tabular表达式.在这里,本文从指称语义的角度给出eval的语义:
eval:KT[Tabular]x{assign(s)}®Value.
文献[18]将类型的概念引入到了Tabular中,从约束谓词、求值方案和辅助函数这3个方面定义Tabular表达式的类型,将具有相同组织形式的不同Tabular表达式划分为同一类型.本文从以下4个方面解读Tabular表达式中类型的语义:
1) 若设Tabular表达式T的指称语义为指引集S,则T的类型需要给出S的维度n;
2) 若AS为Tabular表达式T对应的eval函数的指派集,则T的类型需要给出AS中指派的指派顺序;
3) 若Tabular表达式T索引的Gird集合为{g1,g2,…,gn},则T的类型需要给出gi(1≤i≤n)所对应的公式集合的互斥性与完备性如何;
4) 若Tabular表达式T索引的Gird集合为{g1,g2,…,gn},则T的类型需要给出gi(1≤i≤n)中表达式的具体类型.
Tabular表达式的类型体现了表达式的组织形式和求值策略,从组成和求值两个角度完成对Tabular表达式类别的划分.值得注意的是,表达式的具体类型不仅仅包括标量表达式和Tabular表达式的划分,还包括表达式的具体组织形式.
由于根据Tabular表达式通用模型的定义可以定义无穷种Tabular表达式的类型,因而无法从类型的角度对Tabular表达式的语义进行全面地分析.根据Tabular表达式通用模型的形式文法,可以定义任意类型的Tabular表达式,从Tabular表达式的形式文法分析入手,针对各语法单元给出相应的语义指派方程,可以使Tabular表达式的语义分析不再受类型的限制.任何一种类型的Tabular表达式,只要满足Tabular表达式通用模型的形式文法,就适用于本文的方法.后文将就Tabular表达式通用模型中具有代表性的表对本文方法的有效性进行分析.
3 传统类型Tabular表达式的语义Tabular表达式最初只包含正规函数表、反转函数表、向量函数表等10种表的形式化定义.本节将对传统类型Tabular表达式中一些具有代表性的表类型进行语义描述.
3.1 正规函数表一个正规函数表中包含1个主Grid和n个辅助Grid:主Grid中包含的表达式都是由常量、变量或函数的施用组成,本文将这种表达式统称为算术表达式;辅助Grid中的表达式都是谓词表达式.通常用一个正规函数表来描述一个函数,该函数的定义域是一组赋值,n个辅助Grid描述主Grid各项取值需满足的各种条件,主Grid描述了函数的具体取值结果.图 1是一个正规函数表的例子.
 | Fig. 1 Example of a normal function table 图 1 正规函数表的例子 |
图 1中的正规函数表包含3个Grid,分别是T[0],T[1]和T[2],T[1]和T[2]描述参数可能出现的各种情况,T[0]描述了各种情况下函数f(A,B)的取值.该正规函数表描述的函数为
若设一个正规函数表T由1个主Grid T[0]和n个辅助Grid T[1],T[2],…,T[n]组成,第i(1≤i≤n)个辅助Grid T[i]中包含mi个谓词表达式,S为T对应指称语义的指引集,则正规函数表类型具有如下语义:
1) S中指引的维度为n(n≥1);
2) T的指派顺序为先辅助Grid、后主Grid,T[i](1≤i≤n)的指派间无先后关系;
3) T[i](1≤i≤n)是互斥且完备的;
4) T[i](1≤i≤n)中的表达式为谓词表达式,T[0]中的表达式为算术表达式.
正规函数表T的具体指称语义如下:
· KT[T]={T[1][i1]®T[2][i2]®…®T[n][in]®T[0][i1,i2,…,in]|1≤ij≤mj(1≤j≤n)};
· KG[T[k]](1≤k≤n)=KT[T]xassign(T[k])={T[1][i1]®…®T[k-1][ik-1]®T[k+1][ik+1]®…®T[ n][in]®T[0][i1,…,ik-1,ak,ik+1,…,in]|1≤ij≤mj(1≤j≤n)};
· KG[T[0]]=[KT[T]xassign(T[1])xassign(T[2])x...xassign(T[n])]xassign(T[0])={Value};
· KSE[T[i][j]](1≤i≤n,0≤j≤mi)=assign(T[i])®Bool;
· KSE[T[0][i1,i2,…,in]](1≤ij≤mj,1≤j≤n)=assign(T[0])xassign(T[1])x...xassign(T[n])®Value;
· eval(T)=KT[T]xassign(T[1])xassign(T[2])x...xassign(T[n])xassign(T[0])®Value.
T[i](1≤i≤n)的指派情况将参数映射到具体求值表达式,T[0]的指派情况给出了参数在各种条件下的计算结果.正规函数表的取值结果就是函数针对一组参数赋值的计算结果.对T[0]中表达式的结果进行计算不仅仅需要Grid T[0]的指派,还需要辅助Grid T[i](1≤i≤n)的指派,因为辅助Grid的指派情况决定了表达式的计算结果为空还是具体的值.
上文的Bool代表波尔类型的变量,只能取真值或假值;Value代表一个数值,是算术表达式的计算结果;ak代表assign(T[k])的指派结果.下文在没有特殊说明的情况下,上述符号的意义与此处相同.索引只是为Tabular表达式和Grid,或者为Grid和表达式建立关联,语义并不会随着Tabular表达式类型的变化而发生变化;常量和变量都是构成标量表达式的基本元素,语义也不会随着Tabular表达式类型的变化而变化,因而关于索引、变量和常量的指称语义本文不再重复赘述.
3.2 反转函数表反转函数表同样由1个主Grid和n个辅助Grid组成,与正规函数表不同的是:主Grid中的表达式是谓词表达式,而1个辅助Grid中的表达式是算术表达式,其余n-1个辅助Grid中的表达式是谓词表达式.反转函数表描述的仍然是函数,任何被反转函数表描述的函数都可以用正规函数表来描述.图 2是反转函数表的例子.
 | Fig. 2 Example of an inverted function table 图 2 反转函数表的例子 |
图 2中描述了3个Grid,分别是T[0],T[1]和T[2],T[0]和T[2]描述了参数的各种取值情况,T[1]描述了函数f(x,y)的在各种参数下的具体取值.该反转函数表描述的函数为
若设反转函数表T由1个主Grid T[0]和n个辅助Grid T[1],T[2],…,T[n]组成,T[1]中包含m1个算术表达式,T[i](1≤i≤n)中包含mi个谓词表达式,T[0]中包含m1xm2x...xmn个谓词表达式,S为T对应指称语义的指引集,则反转函数表类型具有如下语义:
1) S中指引的维度为n(n≥1);
2) T的指派顺序是先T[i](2≤i≤n),然后T[0],最后T[1],T[i](2≤i≤n)的指派间无先后关系;
3) T[i](2≤i≤n)是互斥且完备的,T[0]是完备的;
4) T[i](2≤i≤n),T[0]中的表达式是谓词表达式,T[1]中的表达式是算术表达式.
反转函数表T的具体指称语义如下:
· KT[T]={T[2][i2]®T[3][i3]®…®T[n][in]®T[0][i1,i2,i3,…,in]®T[1][i1]}|1≤ij≤mj(1≤j≤n)};
· KG[T[k]](2≤k≤n)=KT[T]xassign(T[k])={T[2][i2]®…®T[k-1][ik-1]®T[k+1][ik+1]®…®T[n][in]®T[0][i1,i2,…,ik-1,ak,ik+1,…,in]®T[1][i1]|1≤ij≤mj(1≤j≤n)};
· KG[T[0]]=[KT[T]xassign(T[2])xassign(T[3])x...xassign(T[n])]xassign(T[0][a2,a3,…,an])={T[1][a1]};
· KG[T[1]]=[KT[T]xassign(T[2])xassign(T[3])x...xassign(T[n])xassign(T[0][a2,a3,…,an])]xassign(T[1]={Value};
· KSE[T[i][j]](2≤i≤n,1≤j≤mi)=assign(T[i])®Bool;
· KSE[T[0][i1,i2,i3,…,in]](1≤ij≤mj,1≤j≤n)=assign(T[2])xassign(T[3])x...xassign(T[n])xassign(T[0][a2,a3,…,an])®Bool;
· KSE[T[1][j]](1≤j≤mi)=assign(T[2])xassign(T[3])x...xassign(T[n])xassign(T[0][a2,a3,…,an])xassign(T[1])®Value;
· eval(T)=KT[T]xassign(T[2])xassign(T[3])x...xassign(T[n])xassign(T[0][a2,a3,…,an])xassign(T[1])®Value.
T[i](2≤i≤n)与T[0]一起给出了函数参数的各种取值情况,T[i]的指派情况将T[0]中的参数取值情况缩至T[0]的一个子网格T[0][a2,a3,…,an]中,T[0][a2,a3,…,an]包含m1个谓词表达式,而T[0][a2,a3,…,an]的指派情况决定了函数最终的计算结果T[1][a1].反转函数表的取值结果eval(T)同样为函数的计算结果.
3.3 向量函数表向量函数表由1个主Grid、1个变量Grid和n-1个辅助Grid组成.主Grid中的表达式为谓词表达式,变量Grid中的表达式为变量,辅助Grid中的表达式为谓词表达式.向量函数表描述的是一个函数,其定义域是一组赋值,值域是n元组的集合,变量Grid用于给出一组赋值,辅助Grid为这组赋值索引赋值被接受应满足的条件,在主Grid中找对应的列,主Grid判断这组赋值是否被该函数所接受.
图 3是向量函数表的例子.
 | Fig. 3 Example of a tuple table 图 3 向量函数表的例子 |
图 3中描述了3个Grid,分别是主Grid T[0]、辅助GridT[1]和变量GridT[2].T[2]给出了函数的定义域,T[1]和T[0]给出了赋值被接受需满足的条件.
若设向量函数表T由主Grid T[0]、辅助GridT[i](1≤i≤n-1)和变量GridT[n]组成,T[i](1≤i≤n-1)中包含mi个谓词表达式,T[i]中包含mn个变量,T[0]中包含m1xm2x.. .xmn个谓词表达式,S为T对应指称语义的指引集,则向量函数表类型具有如下语义:
1) S中指引的维度为n(n≥1);
2) T的指派顺序是先T[n],之后T[i](1≤i≤n-1),最后T[0],T[i](1≤i≤n-1)的指派间无先后关系;
3) T[i](1≤i≤n-1)是互斥且完备的;
4) T[i](0≤i≤n-1)中的表达式是谓词表达式,T[n]中的表达式是变量.
向量函数表T的具体指称语义如下:
· KT[T]={T[1][i1]®T[2][i2]®…®T[n-1][in-1]®T[0][i1,i2,…,in-1,1]ÙT[0][i1,i2,…,in-1,2]Ù...ÙT[0][i1,i2,…,in-1,mn]®Bool|1≤ij≤mj(1≤j≤n)};
· KG[T[k]](1≤k≤n-1)=KT[T]xassign(T[k])={T[1][i1]®…®T[k-1][ik-1]®T[k+1][ik+1]®…®T[n-1][in-1]®T[0][i1,…,ik-1,ak,ik+1,…,in-1,1]ÙT[0][i1,…,ik-1,ak,ik+1,…,in-1,2]Ù...ÙT[0][i1,…,ik-1,ak,ik+1,…,in-1,mn]®Bool|1≤ij≤mj(1≤j≤n)} ;
· KG[T[n]]=[KT[T]xassign(T[1])xassign(T[2])x...xassign(T[n-1])]xassign(T[n])={T[0][a1,a2,…,an-1,1]ÙT[0][a1,a2,…,an-1,2]Ù...ÙT[0][a1,a2,…,an-1,mn]};
· KG[T[0]]=[KT[T]xassign(T[1])xassign(T[2])x...xassign(T[n])]xassign(T[0][a1,a2,…,an-1])={Bool};
· KSE[T[i][j]](1≤i≤n-1,1≤j≤mi)=assign(T[i])®Bool;
· KSE[T[n][j]](1≤j≤mn)=assign(T[i])®Value;
· KSE[T[0][i1,i2,…,in]](1≤ij≤mi,1≤j≤n)=assign(T[1])xassign(T[2])x...xassign(T[n])xassign(T[0][a1,a2,…,an-1])®Bool;
· eval(T)={assign(T[n])|KT[T]xassign(T[1])xassign(T[2])x...xassign(T[n])}xassign(T[0][a1,a2,…,an-1])®true}.
T[i](1≤i≤n-1)的指派情况决定了T[n]中的赋值满足哪些T[0]中的哪些条件才能被接受,T[0]的指派决定了各种条件下赋值变量被接受的具体条件.由于T[i](1≤i≤n-1)的指派将T[n]中赋值被接受的条件缩减至T[0]的一个字网格T[0][a1,a2,…,an-1]中,因而判断T[n]的赋值能否被接受,只需给出T[0][a1,a2,…,an-1]的指派情况,而不需对整个T[0]进行指派.向量函数表的取值结果eval(T)不再是一个具体的值,而是一个能被T[0]所接受的赋值集合.
3.4 决策表决策表包含经典决策表和通用决策表两种类型,任何经典决策表都可以经过等价变换转换为通用决策表.经典决策表由1个主Grid和2个辅助Grid组成,主Grid中的表达式是波尔类型的常量,辅助Grid中的表达式,一个为变量表达式,一个为谓词表达式;通用决策表由1个主Grid和1个辅助Grid组成,主Grid中为谓词表达式,辅助Grid中为算术表达式.图 4和图 5分别是同一个决策表的经典决策表和通用决策表.本文将就通用决策表分析决策表的指称语义.
 | Fig. 4 Example of a classic decision table 图 4 经典决策表的例子 |
 | Fig. 5 Example of a generalized decision table 图 5 通用决策表的例子 |
若设通用决策表T由主Grid T[0]和辅助Grid T[1]组成,T[1]包含m个算术表达式,T[0]中包含nxm(n为等价经典决策表中谓词表达式的数量)个谓词表达式,S为T对应指称语义的指引集,则通用决策表类型具有如下语义:
1) S中指引的维度为n(n≥1);
2) T的指派顺序是先T[0][i](1≤i≤n),再T[1],T[0][i]的指派间无先后关系;
3) T[0][i]是完备的;
4) T[0]中的表达式是谓词表达式,T[1]中的表达式为算术表达式.
通用决策表T的具体指称语义如下:
· KT[T]={T[0][1,i0]®T[0][2,i1]®…®T[0][n,in]®T[1][k]|1≤ij≤mj(1≤j≤n),1≤k≤m};
· KG[T[0]]=KT[T]xassign(T[0][1])xassign(T[0][2])x...xassign(T[0][n])={T[1][a1]};
· KG[T[1]]=[KT[T]xassign(T[0][1])xassign(T[0][2])x...xassign(T[0][n])]xassign(T[1])={Value};
· KSE[T[0][i,j]](1≤i≤n,1≤j≤m)=assign(T[0][i])®Bool;
· KSE[T[1][j]](1≤j≤m)=assign(T[0])xassign(T[1])®Value;
· eval(T)=KT[T]xassign(T[0][1])xassign(T[0][2])x...xassign(T[0][n])xassign(T[1])®Value.
决策表描述了一件事务的决策过程,T[0]给出了影响该事务的各种因素,T[1]给出了各种条件下,该事务实施的各种操作.T[0]指派情况决定了T[1]中操作的选择情况,T[1]的指派情况决定整个事务的决策结果.决策表的取值结果eval(T)就是事务的决策结果.
4 扩展类型Tabular表达式的语义上一节对一些传统类型Tabular表达式的语义进行了描述,但通用模型不仅仅包含传统类型的10种表,还包含无穷种自定义表类型.本节将对一些根据通用模型自定义的Tabular表达式进行语义描述,进一步说明本文方法的适用性与一般性.
4.1 冗余信息表冗余信息表中包含1个主Grid和4个辅助Grid,主Grid T[0]中存放的表达式为常量,辅助Grid T[i](1≤i≤4)中存放的是谓词表达式,其中,T[1]和T[3]是对同一组谓词公式的不同描述,T[2]和T[4]也是对同一组谓词公式的不同描述.图 6是一个冗余信息表的例子,该表描述的是服装店对一款热销上衣的尺码推荐信息,T[1]和T[3]分别用千克和磅两种单位描述了体重信息,T[2]和T[4]分别用英寸和厘米描述了身高信息,T[3]根据顾客身高和体重的信息对衣服的尺码进行推荐.
 | Fig. 6 Example of a tabular expression with redundant headers 图 6 冗余信息表的例子 |
若设一个冗余信息表T由主Grid T[0]和辅助Grid T[i](1≤i≤4)组成,T[1]和T[3]描述同一组谓词表达式, T[2]和T[4]描述同一组谓词表达式,T[1]和T[3]中包含m个谓词表达式,T[2]和T[4]中包含n个谓词表达式,T[0]中包含nxm个常量,S为T对应指称语义的指引集,则冗余信息表类型具有如下语义:
1) S中指引的维度为2;
2) T的指派是任意2个描述不同组谓词表达式的辅助Grid的指派,二者无先后顺序;
3) T[i](1≤i≤4)是互斥的;
4) T[0]中的表达式为常量,T[i](1≤i≤4)中的表达式为谓词表达式.
冗余信息表T的具体指称语义如下:
· KT[T]={T[1][i]ÚT[3][i]®T[2][j]ÚT[4][j]®T[0][i,j]|1≤i≤m,1≤j≤n};
· KG[T[0]]=[KT[T]xassign(T[1])xassign(T[2])]+[KT[T]xassign(T[1])xassign(T[4])]+[KT[T]xassign(T[3])xassign(T[2])]+[KT[T]xassign(T[3])xassign(T[4])]={Constant};
· KG[T[i]](i=1Úi=3)=[KT[T]xassign(T[2])]+[KT[T]xassign(T[4])]={T[2][j]ÚT[4][j]®T[0][i,j]|1≤j≤n};
· KG[T[i]](i=2Úi=4)=[KT[T]xassign(T[1])]+[KT[T]xassign(T[3])]={T[1][j]ÚT[3][j]®T[0][i,j]|1≤j≤m};
· KSE[T[i][j]](i=2Úi=4,1≤j≤m)=assign(T[i])®Bool;
· KSE[T[i][j]](i=1Úi=3,1≤j≤n)=assign(T[i])®Bool;
· KSE[T[0][i,j]](1≤i≤n,1≤j≤m)=Constant;
· eval(T)=[KT[T]xassign(T[1])xassign(T[2])]+[KT[T]xassign(T[1])xassign(T[4])]+[KT[T]xassign(T[3])xassign(T[2])]+[KT[T]xassign(T[3])xassign(T[4])]®Constant.
冗余信息表中描述冗余信息(同一组谓词表达式的不同描述)的Grid不仅仅可以是2个,也可以是多个,推荐结果的前提条件也可以是多个.事务被执行的前提是满足多个条件中的一个,这种情况适合用冗余信息表来描述.
4.2 循环表循环表中包含1个主Grid和n个辅助Grid,主Grid中的表达式可以是任意类型,包括Tabular表达式,辅助Grid中的表达式为谓词表达式.当主Grid中的表达式为算术表达式时,循环表的功能和正规函数表很相似,但正规函数表中辅助Grid的指派间是相互独立的,而循环表中T[i]的指派会影响T[i+1]的指派.图 7给出了一个循环表的例子,图中的循环表包含1个主Grid T[0]和3个辅助Grid T[i](1≤i≤3),T[1]的指派影响T[2]的指派,T[2]的指派影响T[3]的指派,T[3]的指派影响循环表的最终取值结果.
 | Fig. 7 Example of a circular table 图 7 循环表的例子 |
若设一个循环表T由1个主Grid T[0]和n个辅助Grid T[1],T[2],…,T[n]组成,第i(1≤i≤n)个辅助GridT[i]中包含mi个谓词表达式,Grid T[0中包含mn个谓词表达式,T[i,i-1]为T[i]中受T[i-1,i-2]的指派情况影响的谓词表达式的集合,S为T对应指称语义的指引集,则循环表类型具有如下语义:
1) S中指引的维度为n;
2) T的指派顺序为T[1],T[2],....,T[n],最后为T[0];
3) T[i](1≤i≤n是互斥的;
4) T[0]中的表达式为任意类型,T[i](1≤i≤n)中的表达式为谓词表达式.
为了方便说明,下面将就T[0]中的表达式为算术表达式的情况说明循环表T的指称语义:
· KT[T]={T[1][i1]®T[2][i2]®…®T[n][in]®T[0][in]|1≤ij≤mj(1≤j≤n)};
· KG[T[k]](1≤k≤n)=[KT[T]xassign(T[1])xassign(T[2,1])x…xassign(T[k-2,k-1])]xassign(T[k-1,k])={T[k+1][ik+1]®…®T[n][in]®T[0][in]|1≤ij≤mj(1≤j≤n)};
· KG[T[0]]=[KT[T]xassign(T[1])xassign(T[2,1])x...xassign(T[n,n-1])]xassign(T[0])={Value};
· KSE[T[i][j]](1≤i≤n,0≤j≤mi)=assign(T[i])®Bool;
· KSE[T[0][j]](1≤j≤mn)=assign(T[1])xassign(T[2,1])x...xassign(T[n,n-1]xassign(T[0])®Value;
· eval(T)=KT[T]xassign(T[1])xassign(T[2,1])x...xassign(T[n,n-1]xassign(T[0])®Value.
循环表中,每一个辅助Grid T[i]中表达式的取值不仅受自身指派情况的影响,还与前i-1个辅助Grid的指派情况有关.n个辅助Grid的指派情况和主Grid的指派情况共同影响T[0]中表达式的计算结果,进而影响循环表的取值情况.
5Tabular表达式语义描述方法的比较从本质上说,当前Tabular表达式语义模型的研究可以分为以下3个角度:1) 基于函数和关系的联合单独定义每一个表的语义;2) 通过定义如何求值给出表达式的语义;3) 从功能的角度给出Tabular表达式中各语法单位的形式语义.只是每种语义模型针对的Tabular表达式模型有所差别,进而导致了语义模型在适用性和扩展性上有所差别.表 2给出了当前主流Tabular表达式语义描述方法的比较.
|
|
Table 2 The comparison of different semantic description methods of tabular expressions 表 2 Tabular表达式不同语义描述方法的比较 |
最初的Tabular表达式只有10种表,没有统一的模型对其进行描述,只能通过单独定义函数或关系的联合对每个表的语义进行描述,因而该方法的形式化程度较低.Jancki,Abraham和Kahl等人分别基于早期的10种表给出了各自统一的形式化模型,并都从如何求值的角度对Tabular表达式的语义进行了研究.Jancki和Abraham的模型很相近,因此后来有学者将二者的模型统称为J-A模型.J-A模型由原始结构、谓词规则、关系规则、单元连接图、单元到表达式的映射以及复合操作组成,该模型根据单元连接图、表谓词规则和表关系规则为表中每一个元素定义一种关系,利用所有元素对应关系的复合来反映Tabular表达式的语义;在Kahl模型中,Tabular表达式是由表和一组语义规则构成,表可以通过增加标题和表连接的操作,由单元组成的表逐步构造而成,而语义规则体现了表达式的求值结构,该模型的语义解释是通过应用结构化归约把表格映射到值.
与本文方法相比,这3种方法的主要缺陷在于Tabular表达式形式化模型本身的缺陷.从本质上讲,这3种方法都将Tabular表达式的结构定义成一个由主网格和若干标题网格组成的多维矩形结构,并要求主网格索引集合是其他标题网格索引集合的笛卡尔乘积,索引集合都是连续整数集合,而且它们对形式语义的定义也依赖于这种物理表示结构.本文方法针对Tabular表达式通用模型,该模型不依赖于特定的物理表示结构,对于同一个Tabular表达式定义,可以由不同的物理布局形式,具有良好的扩展性,可以定义新的表类型,如上文提到的冗余信息表、循环表等,都是其他模型无法表示的.
Tabular表达式通用模型由Parnas教授和金英教授共同给出,他们从如何求值的角度对Tabular表达式通用模型的操作语义进行了研究.本文从指称语义的角度分析了Tabular表达式通用模型的形式语义,从理论上讲,操作语义与指称语义的描述能力是等价的,但是Tabular表达式通用函数的操作语义描述需要针对特定的类型, Tabular表达式通用模型中包含无穷种类型,无法一一穷举,这为相关应用工具的开发造成了很大困难,每当需要在工具中增加新类型时,都会伴随着大量的改动.本文的研究依赖于Tabular表达式通用模型的形式文法,可以随时根据应用创建满足Tabular表达式通用模型形式文法的任意类型,使得Tabular表达式相关分析验证工具的开发不再受类型的限制,为Tabular表达式通用模型的进一步推广奠定了良好的基础.
6 结束语本文基于Tabular表达式通用模型给出了其形式文法,并首次从指称语义的角度Tabular表达式的语义描述方法进行了研究.分别从传统类型Tabular表达式和新类型Tabular表达式两个角度对本文的语义描述方法进行了验证,研究分析表明:本文的方法不再受Tabular表达式模型和类型的限制,打破了现有方法的局限性,为Tabular表达式通用模型的推广和相关分析验证工具的开发奠定了良好的基础.
| [1] | Jin Z, Liu L, Jin Y. Software Requirements Engineering: Principles and Methods. Beijing: Science Press, 2008. 282-299 (in Chinese). |
| [2] | Heninger KL, Kallander J, Parnas DL, Shore JE.Software requirements for the A-7E aircraft. NRL Report 9194, U.S. Naval Research Lab., 1978. |
| [3] | Heninger KL. Specifying software requirements for complex systems: New techniques and their applications. IEEE Trans. on Software Engineering, 1980,SE-6(1):2-13 . |
| [4] | Parnas DL. Software aspects of strategic defense systems.Communications of the ACM, 1985,28(12):1326-1335 . |
| [5] | Parnas DL, Asmis GLK, Madey J.Assessment of safety-critical software in nuclear power plants. Nuclear Safety, 1991,32(2): 189-198. |
| [6] | Parnas DL. Inspection of safety critical software using function tables. In: Proc. of the IFIP World Congress. Vol.3. 1994. 270-277. |
| [7] | Parnas DL, Madey J. Functional documentation for computer systems engineering. Science of Computer Programming, 1995, 25(1):41-61. |
| [8] | Parnas DL, Madey J, Iglewski M.Precise documentation of well-structured programs. IEEE Trans. on Software Engineering, 1994,20(12):948-976 . |
| [9] | Parnas DL. Document based rational software development. Knowledge-Based Systems, 2009,22(3):132-141 . |
| [10] | Degiovanni R, Ponzio P, Aguirre N, Frias M. Abstraction based automated test generation from formal tabular requirements specifications. LNCS 6706: Tests and Proofs, 2011. 84-101 . |
| [11] | Feng X, Parnas DL, Tse TH. Fault propagation in Tabular expression-based specifications. In: Proc. of the 32nd Annual IEEE Int’l Computer Software and Applications Conf. 2008. 180-183 . |
| [12] | Herrmannsdörfer M, Konrad S, Berenbach B. Tabular notations for state machine-based specifications. Crosstalk, 2008,21(3): 18-23. |
| [13] | Peters DK, Lawford M, Widemann BT. An IDE for software development using Tabular expressions. In: Proc. of the 2007 Conf. of the Center for Advanced Studies on Collaborative Research. 2007. 248-251 . |
| [14] | Janicki R. Towards a formal semantics of Parnas tables. In: Proc. of the 17th Int’l Conf. on Software Engineering. 1995. 231-240 . |
| [15] | Janicki R, Khedri R. On a formal semantics of Tabular expressions. Science of Computer Programming, 2001,39(2-3):189-213 . |
| [16] | Abraham RF.Evaluating Generalized Tabular Expressions. McMaster University Canada, 1997. |
| [17] | Kahl W. Compositional syntax and semantics of tables. Technical Report, SQRL 15, Software Quality Research Laboratory, McMaster University Canada, 2003. |
| [18] | Jin Y, Parnas DJ. Defining the meaning of Tabular mathematical expressions. Science of Computer Programming, 2010,75(11): 980-1000 . |
| [1] | 金芝,刘璘,金英.软件需求工程:原理和方法.北京:科学出版社,2008.282-299. |