领域数据建模是制定和验证行业数据规范的基础.数据规范的制定, 对行业信息化建设起到指导作用, 对行业数据的分析和基于数据分析的决策至关重要.大规模分布式复杂应用系统是目前应用系统的主流, 随着应用系统规模的逐渐增大, 行业数据规范制定越来越复杂, 特别是数据规范编写满足需求的验证也变得复杂和困难.传统的人工编写方法难以应对这种复杂性, 研发行业数据规范形式化编写方法和自动化验证方法, 成为今后必然的发展趋势.

作为一种轻量级形式化方法, 类型系统研究始于20世纪初, 到70年代已成为证明论中的标准工具, 也是程序设计语言的基础^[1].类型理论通过类型、求值和类型规则的定义和解释, 研究项的可类型化和项的良类型等性质.类型系统通过静态检查可以检查错误, 通过抽象还可以强化规范编程.一个软件系统中出现的任何一个数据或程序片段都可以认为是项, 因此, 类型理论可以作为领域数据建模的理论基础, 通过构造一个类型系统, 可以进行领域数据建模并进行验证.

本文面向行业数据规范及其验证, 通过分析应用需求和行业数据特点, 提出了一种基于类型理论的领域数据建模语言(domain data modelling language, 简称DDML)和领域数据建模方法(domain data modelling method, 简称DDMM), 并将其应用于实际规模的应用案例中, 说明了该方法的有效性.为此, 本文第1节综述类型理论的研究现状.第2节的DDML语言定义了类型和项的语法和语义, 以及类型规则及其类型检查算法.DDMM方法则给出了领域数据建模的步骤, 即构建𝒦₁(原子类型)、𝒦₂(数据元)、𝒦₃(数据元目录)3层框架, 以及如何生成表示𝒦₃层数据元目录之间关系的类型规则.在此基础上, 给出数据元目录序列的定义及其正确性判定算法.第3节面向某行业实际数据规范的制定与验证, 通过需求分析, 采用领域数据建模工具原型系统进行数据建模和验证.最后一节给出本文在理论和应用上的主要贡献.

1 相关研究

程序设计语言的设计是类型理论中重要的应用领域^[2], 从FORTRAN语言中引入类型开始^[3], 类型理论成为了结构化程序设计语言^[4]、面向对象程序设计语言^[5]以及函数式程序设计语言^[6]的理论基础.此外, 类型系统也用于静态分析程序正确性^[7]、分析移动计算运行时的正确性^[8]、程序行为分析^[9]以及用于定义程序中的数据处理模式^{[10, 11]}.此外, 在大数据处理与分析领域, 研究人员通过定义一般类型和线性类型及其类型规则, 可以严格定义大数据处理中的并行计算过程, 将Map-Reduce转化为不同类型的类型映射之和, 从而可以将一个任务分而治之^[12].类型理论的研究正趋于解决前沿的工程与技术问题.

领域数据建模是描述一个行业的数据以及数据之间关系的方法, 是数据库、信息系统、软件工程和知识表示等领域中重要的基础工作.ER模型是早期的数据建模方法, 可以描述实体、属性和关系^[13].采用ER建模已成为关系数据库设计与开发的起点, 但该模型在关系上主要关注实体之间的主外键关系.面向对象建模方法的产物——统一建模语言(UML), 在数据建模中能够描述丰富的关系, 但其对数据的约束和值域的描述相对复杂^[14].一种描述逻辑数据建模方法^[15]扩充了ER模型和面向对象建模方法的描述能力, 并提供了基本的推理功能, 但其逻辑符号相对复杂, 且更侧重于数据库中对Schema的一致性验证.一种多维数据建模方法主要用于联机分析处理(OLAP)中对多维复杂数据的建模^[16].基于概念聚类机制(CCM)的数据模型则通过簇和角色的动态定义, 主要用于视频数据库的数据建模^[17].此外, 类型描述语言PCT, 利用高级程序设计语言和一阶谓词逻辑可以描述数据模型中的类型、语义特征和完整性约束^[18], 但其数据描述能力和应用规模有限.数据建模的理论的方法众多, 但是能够简洁而精确地描述一个行业数据的构造过程和关系的方法还并不多见.

类型系统作为一种轻量级形式化方法, 通过类型规则可以构造复杂类型及它们之间的关系, 通过类型检查算法可以判定一个给定项的类型以及给定类型之间的关系是否满足^[1].为了解决应用中大规模实际问题, 本文采用类型理论作为数据建模及其验证的理论基础, 研究领域数据建模语言、领域数据建模方法及其验证方法, 并开发相应的原型系统工具, 以支持领域数据建模和自动化验证.

2 领域数据建模语言和方法

领域数据建模语言包括类型、类型语义、项、环境、类型规则、项语义这6个组成部分.

2.1 类型

DDML语言中的类型记为X, 其类型表达式定义如下:

$ X:: = T\left| {\left\{ {l:T} \right\}} \right|T\;\;{\rm{with}}\;\;\left\langle {constraint} \right\rangle \left| {{T^*}} \right|\left\{ T \right\}|{T_1} \times {T_2}\left| {{T_1} + {T_2}} \right|{T_1} \to {T_2}, $

其中, T, T₁, T₂均为类型.

(1) 如果l是标签, 则{l:T}也是类型;

(2) 如果t:T, 并且t满足〈constraint〉的约束, 则T with 〈constraint〉也是类型.其中, 约束constraint::=τ并且τ::=φ|x|c|f(τ₁, …, τ_n)|τ₁∧τ₂|¬ τ, φ为空, x是变量符号, c是常量符号, f是n元函数(或关系)符号;

(3) T^*表示类型的幂, T^*也是类型;

(4) {T}表示一个成员组成的元组类型;

(5) T₁×T₂表示类型的聚合也是类型;

(6) T₁+T₂表示类型的和也是类型;

(7) T₁→T₂表示类型之间的映射也是类型.

其中, 类型T₁×T₂也可以写为{T₁, T₂}.

对上述语法定义举例说明如下.

1) 带标签的类型{l:T}, 是对类型T加注了标签名称, 旨在突出使用用途.例如, 如果有类型integer, 则{count:integer}也是一种类型, 可以用于表示计数的整数类型;

2) 带约束的类型T with 〈constraint〉, 是对类型T, 通过增加约束, 限定其可能取值.例如, 对于t:integer, 如果t满足〈length(t)=number〉约束, 则t:integer with 〈length(t)=number〉, 即长度为number的整数;

3) 幂类型T^*, 是在类型T的基础上构造的类型, 使用较为普遍.例如字符串类型string实为字符类型char的幂类型;

4) 单元组类型{T}, 是一种特殊的元组类型, 只有一个成员, 其类型为T.单元组类型在面向对象编程中相当于具有一个成员变量的类.例如, {integer}是单元组类型;

5) 类型的乘积T₁×T₂, 是在类型T₁和T₂的基础上构造的多元元组类型, 类似于面向对象编程中的封装;

6) 类型的和T₁+T₂, 是在类型T₁和T₂的基础上构造的类型, 用于扩展可能取值;

7) 类型映射T₁→T₂, 是一种函数类型, →左端表示输入, →右端表示输出.例如, string→integer可以表示输入参数为string, 输出参数为integer的所有函数的类型.

2.2 类型语义

设||T||表示类型T的值域, 则DDML语言的类型语义定义如下.

(1) ||{l:T}||={{l=a}|a∈||T||};

(2) ||T with 〈constraint〉||={constraint(a)|a∈||T||};

(3) ||T^*||=||T||^*, 其中, 等式右上角的符号“^*”表示集合幂集;

(4) ||{T}||={{a}|a∈||T||};

(5) ||T₁×T₂||=||T₁||×||T₂||, 其中, 等式右边的符号“×”表示集合的笛卡尔积;

(6) ||T₁+T₂||=||T₁||$ \cup $ ||T₂||, 其中, 等式右边的符号“$ \cup $”表示集合的并;

(7) ||T₁→T₂||=||T₁||→||T₂||, 其中, 等式右边的符号“→”表示集合之间的映射.

注:由上述定义, ||T with 〈constraint〉||表示||T||中所有被〈constraint〉约束的元素的集合.

对上述语义举例说明如下.

1) 带标签的类型, 其语义||{l:T}||的值域集合, 与语义||T||的值域集合相同, 只是值域集合中的每个元素的形式写为{l=a};

2) 带约束的类型, 其语义||T with 〈constraint〉||的值域集合, 是语义||T||的值域集合的子集;

3) 幂类型, 其语义||T^*||的值域集合, 是语义||T||的值域集合的幂集;

4) 元组类型, 其语义||{T}||的值域集合, 是语义||T||的值域集合中每个元素加元组符号{}的集合;

5) 乘积类型, 其语义||T₁×T₂||的值域集合, 是语义||T₁||的值域集合和语义||T₂||的值域集合的笛卡尔积;

6) 和类型, 其语义||T₁+T₂||的值域集合, 是语义||T₁||的值域集合和语义||T₂||的值域集合的并集;

7) 映射类型, 其语义||T₁→T₂||的值域集合, 是语义||T₁||的值域集合到语义||T₂||的值域集合的映射.

2.3 项

DDML语言的项t定义如下:

$ t:: = x\left| c \right|\left\{ {l = t} \right\}\left| {\left( {{t_1}, \ldots , {t_n}} \right)} \right|f\left( {{t_1}, \ldots , {t_n}} \right)\left| {t\left( u \right)} \right|t\;\;{\rm{as}}\;\;T|{\rm{if}}\;\;{t_1}\;\;{\rm{then}}\;\;{t_2}\;\;{\rm{else}}\;{t_3}. $

2.4 环境

DDML语言的环境Γ是变量绑定的序列, 定义为

$ \mathit{\Gamma} :: = \emptyset |\mathit{\Gamma} , t:T $

为方便起见, 一个非空的环境Γ经常写为t₁:T₁, …, t_n:T_n, n≥1.

2.5 类型规则

在环境Γ中, 一个判定形为Γ|-t:X.通过判定该语言的类型表达式或项是否满足给定的类型规则, 可以验证期望的性质.其类型规则可以分为结构类规则和关系类规则.

●结构类规则

$ \frac{{{a_1}:T, ..., {a_n}:T, 对于任意n \ge 1}}{{{a_1}...{a_n}:{T^*}}} $

(TR1)

$ \frac{{x:A, x满足\langle constraint\rangle }}{{{\rm{ }}x:A{\rm{ with }}\langle constraint\rangle }} $

(TR2)

$ \frac{{t:T, l\;{\rm{ is}}\;\;{\rm{ a }}\;\;{\rm{label}}}}{{\{ l = t\} :\{ l:T\} }} $

(TR3)

$ \frac{{{a_1}:{T_1}, ..., {a_n}:{T_n}, 对于任意n \ge 1}}{{({a_1}, ..., {a_n}):{T_1} \times ... \times {T_n}}} $

(TR4)

$ \frac{{{v_1}:B, ..., {v_n}:B, T = \{ B\} }}{{{v_1}:T, ..., {v_n}:T}} $

(TR5)

$ \frac{{{t_1}:{B_1}, ..., {t_n}:{B_n}, n \ge 1}}{{range\_{\rm{exp}}({t_1}, ..., {t_n}):B}} $

(TR6)

$ \frac{{t = range\_{\rm{exp}}({t_1}, ..., {t_n}):B, T = \{ B\} }}{{t:T}} $

(TR7)

为下面行文方便, 由类型规则(TR5)和(TR6)引入枚举类型和值域表达式类型.称T为枚举类型, 如果v₁:T, …, v_n:T.由不同类型的项t₁:T₁, …, t_n:T_n组成的表达式range_exp(t₁, …, t_n)表示的项的类型称为值域表达式类型.

对结构类规则(TR2)举例说明如下:

$ \frac{{t:integer, t{\rm{ }}满足\langle length(t) = number\rangle }}{{t:integer{\rm{ with }}\langle length(t) = number\rangle }}. $

为了定义关系类类型规则, 首先给出如下定义.

(1) 聚合关系.如果T=T₁×…×T_i×…×T_n, 1≤i≤n, 称类型T_i和类型T满足聚合关系, 记为${{T}_{i}}\xrightarrow{◇}T$;

(2) 类关联关系.如果R=T₁.i, R=T₂.j, 则称类型T₁和类型T₂通过类型R关联, 记为$ {{T}_{1}}\overset{R}{\longleftrightarrow}{{T}_{2}}$;

(3) 对象关联关系.如果a:R且${{T}_{1}}\overset{R}{\longleftrightarrow}{{T}_{2}}$, 则称类型T₁和类型T₂之间关于对象a关联, 记为${{T}_{1}}\overset{a\text{ }:\text{ }R}{\longleftrightarrow}{{T}_{2}} $;

(4) 枚举关联关系.如果B为枚举类型, 即v₁:B, …, v_n:B, 并且B=T₁.i, T₂={B}, 则称类型T₁和类型T₂满足枚举关联关系, 记为${{T}_{1}}\xrightarrow{\{{{v}_{1}}, ..., {{v}_{n}}\}/\langle \langle enum\rangle \rangle }{{T}_{2}} $;

(5) 值域关联关系.如果range_exp:B, 并且B=T₁.i, T₂={B}, 则称类型T₁和类型T₂满足值域关联关系, 记为$ {{T}_{1}}\xrightarrow{range\_\text{exp}:B/\langle \langle range\rangle \rangle }{{T}_{2}}$.其中, 值域表达式range_exp::=t, t是第2.3节中定义的项.

对上述5种关系, 有如下关系类的类型规则:

●关系类规则

$ \frac{T={{T}_{1}}\times ...\times {{T}_{i}}\times ...\times {{T}_{n}}, 1\le i\le n}{{{T}_{i}}\xrightarrow{◇}T或T.i\xrightarrow{◇}T} $

(TR8)

$ \frac{\text{ }R={{T}_{1}}.i, R={{T}_{2}}.j}{{{T}_{1}}\overset{R}{\longleftrightarrow}{{T}_{2}}} $

(TR9)

$ \frac{\text{ }a:R, R={{T}_{1}}.i, R={{T}_{2}}.j}{{{T}_{1}}\overset{a}{\longleftrightarrow}{{T}_{2}}}\left( 或\frac{\text{ }a:R, {{T}_{1}}\overset{R}{\longleftrightarrow}{{T}_{2}}}{{{T}_{1}}\overset{a}{\longleftrightarrow}{{T}_{2}}} \right) $

(TR10)

$ \frac{{{v}_{1}}:B, ..., {{v}_{n}}:B, B={{T}_{1}}.i, {{T}_{2}}=\{B\}}{{{T}_{1}}\xrightarrow{\{{{v}_{1}}, ..., {{v}_{n}}\}/\langle \langle enum\rangle \rangle }{{T}_{2}}} $

(TR11)

$ \frac{t=range\_\text{exp}({{t}_{1}}, ..., {{t}_{n}}):B, B={{T}_{1}}.i, {{T}_{2}}=\{B\}}{{{T}_{1}}\xrightarrow{range\_\text{exp}/\langle \langle range\rangle \rangle }{{T}_{2}}} $

(TR12)

2.6 项语义

DDML语言的项语义定义如下.

(1) 设Γ|-x:T, 则y∈||T||, 即, 变量符号x的语义是||T||中的变量y;

(2) 设Γ|-c:T, 则u∈||T||, 即, 常量符号c的语义是||T||中的某个常量u;

(3) 设{l=a}:{l:T}, 则{l=u}∈||{l:T}||, u∈||T||;

(4) 设Γ|-t₁:T₁, …, t_n:T_n, 则(v₁, …, v_n)∈||T₁||×…×||T_n||, 其中, v₁∈||T₁||, …, v_n∈||T_n||, “×”表示集合的笛卡尔积;

(5) 设Γ|-t₁:T₁, …, t_n:T_n, 则||f(t₁, …, t_n)||=||f||(v₁, …, v_n), 其中, v₁∈||T₁||, …, v_n∈||T_n||, ||f||是||T₁||×…×||T_n||上的映射, “×”

表示集合的笛卡尔积;

(6) ||t(u)||=||t||(||u||);

(7) ||t as T||=v, v∈||T||;

(8) ||if t₁ then t₂ else t₃||=if ||t₁|| then ||t₂|| else ||t₃||.

2.7 基于类型理论的领域数据建模方法

为领域数据建模和算法描述方便, 本文对DDML中的类型细分为原子类型、基本类型和复合类型, 依次对应于行业数据规范中的原子类型、数据元和数据元目录.可详细定义如下:

定义1(原子类型).原子类型是应用给定的有限多个类型.

例如, 在应用中可以定义string, integer, float, date, datetime, boolean, binary, Digit, Alphabet和Nat为原子类型.

定义2(数据元). (1)数据元可以是由原子类型加约束(类型规则TR3), 并且加标签(类型规则TR1)构成的类型, 其中约束可以为空; (2)数据元可以是枚举类型; (3)数据元可以是值域表达式类型.

定义3(数据元目录).数据元目录是由基本类型聚合而成(类型规则TR4), 或者由某个枚举类型或值域表达式构造而成(类型规则TR5或TR6, TR7)的类型.

后面行文中, 一律采用如上应用中的术语原子类型、数据元和数据元目录.

下面给出领域数据建模方法的建模框架.

● 𝒦₁={A₁, …, A_m};

● 𝒦₂={B₁, …, B_n|B_j={l:A_i with 〈constraint〉}, 1≤j≤n, 1≤i≤m};

● 𝒦₃={T₁, …, T_x|T_j=B_j1×…×B_jk or T_j={P_k} or T_j={E_k}, 1≤j≤x, 1≤k≤n}, 其中, {P_k}由类型规则(TR5)定义, {E_k}由类型规则(TR6)和(TR7)定义.

𝒦₁称为原子类型层, 𝒦₂称为数据元层, 𝒦₃称为数据元目录层.𝒦₁, 𝒦₂, 𝒦₃的构造称为领域数据建模框架, 𝒦= 𝒦₁→𝒦₂→𝒦₃称为领域数据模型.如图 1所示.

图 1给出的DDMM方法包括4个部分, 分别为:1)原子类型建模; 2)数据元建模; 3)数据元目录建模; 4)确定数据元目录之间的关系.其中:第一层表示数据模型中的所有原子类型A₁, …, A_m, m≥1;第二层表示数据模型中的所有数据元, B₁, …, B_n, n≥1(基本类型), P₁, …, P_s, s≥0(枚举类型)以及E₁, …, E_h, h≥0(值域表达式类型); 第三层表示模型中的所有数据元目录T₁, …, T_x, x≥1(复合类型)及其他们之间的关系, 数据元目录相当于类型理论中的记录^[1], 它们之间的关系包括类型关联、枚举关联以及值域关联.模型中还包括两类层间关系, 分别是第三层与第二层之间的聚合关联和第二层与第一层之间的约束关联, 它们都是构造数据元目录的基础.而数据元目录之间的关系决定所建数据模型是否满足业务需求.

定义4(数据元目录序列).设T_k(k=1, …, n)是数据元目录, 则T₁; …; T_n称为一个数据元目录序列, 并且存在T_i和T_j(1≤i, j≤n)满足如下类型关系之一.

●类关联关系: ${{T}_{i}}\overset{R}{\longleftrightarrow}{{T}_{j}}$;

●对象关联关系: ${{T}_{i}}\overset{a\text{ }:\text{ }R}{\longleftrightarrow}{{T}_{j}} $;

●枚举关联关系: ${{T}_{i}}\xrightarrow{\{{{v}_{1}}, ..., {{v}_{n}}\}/\langle \langle enum\rangle \rangle }{{T}_{j}} $;

●值域关联关系: ${{T}_{i}}\xrightarrow{range\_\text{exp}:E/\langle \langle range\rangle \rangle }{{T}_{j}} $.

定义5.设{R₁, …, R_k}是如上定义的数据元目录序列T₁; …; T_n对应的类型关系的集合, 则T₁; …; T_n正确当且仅当R₁∧…∧R_k成立.

2.8 类型检查算法

类型检查算法的目的是判断Γ|-t:T是否成立, 即:对任意给定的一个项t, 判定其类型是否为T.为此, 首先为每一条类型规则TR1~TR7定义其同名类型检查算法^[19];然后, 分别定义原子类型及约束检查算法(CheckAtomicNConstraints)、数据元检查算法(CheckBasicType)、数据元目录检查算法(CheckComposedType); 最后, 利用上述3个算法实现对任意一个项t判定其类型是否为T的检查算法(CheckType).为便于描述算法的时间和空间复杂度, 将模型中的原子类型、数据元、数据元目录、约束、标签以及类型规则的个数分别记为C, N, M, H, K和P, 这些参数刻画了领域问题规模.每一条类型规则TRi同名类型检查算法的时间和空间复杂度在文献[19]中给出.下面给出对于任意给定的项t, 其类型检查算法CheckType及时间和空间复杂度说明.其具体流程见算法1.

算法1. CheckType.

Input: t;

Output: T.

1.   begin

2.    ResultList=null; //初始化结果集

3.    ResultList=CheckComposedType(t); //判断输入项是否为数据元目录

4.    if (ResultList!=null)输出ResultList中的t:T else继续执行步骤5

5.    ResultList=CheckBasicType(t); //判断输入项是否为数据元

6.    if (ResultList!=null)输出ResultList中的t:T else继续执行步骤7

7.    ResultList=CheckAtomicNConstraints(t); //判断输入项是否为原子类型或某个原子类型加约束的类型

8.    if (ResultList!= null)输出ResultList中的t:T else继续执行步骤9

9.   输出受阻

10.   end

根据算法1中的逻辑, 该算法调用了其他3个类型检查子算法.假设其所调用的3个子算法的时间复杂度分别为O_T1, O_T2, O_T3, 则算法1的时间复杂度为O_T1, O_T2, O_T3中的最高者.类似地, 假设其所调用的3个子算法的空间复杂度分别为O_S1, O_S2, O_S3, 则算法1的空间复杂度为O_S1, O_S2, O_S3中的最高者.即, 算法1的时间和空间复杂度相当于该算法所调用的3个子算法时间和空间复杂度中的的最大值.下面分别给出3个子算法的定义及其时间和空间复杂度.

(1) 子算法1

CheckAtomicNConstraints为原子类型及约束检查算法, CheckAtomicNConstraints算法通过判定输入项所属的原子类型A_i及所有满足的约束C_j(j≥0)(约束可以为空), 给出该输入项所属的类型A_i with 〈C_j〉(i≥1, j≥0), 约束可以为空.该算法定义如下.

算法2. CheckAtomicNConstraints.

Input: t;

Output: T.

1.    begin

2.    ResultList=null; //初始化结果集

3.   ResultList=TR2(t); //判断输入项是否为原子类型或原子类型加约束的类型

4.   if (ResultList!=null)输出ResultList中的t:T else继续执行步骤5

5.   输出受阻

6.    end

根据上述算法的逻辑和文献[19]中TR2检测算法的定义, 其时间复杂度O_T1为O(C×H), 空间复杂度O_S1为O(1).

(2) 子算法2

CheckBasicType为数据元检查算法, 该算法通过判定输入项是否为带标签的数据元, 处理其标签后面的项t' 的类型B', 并通过判断{l=t' }:{l:B' }中的{l:B' }是否存在于所有数据元集合中:如果存在, 则认为输入项的类型为{l:B' }所定义的数据元B_k(k≥1), 此外, 数据元检查中还可以检查输入项是否为一个枚举类型值或一个值域表达式的项.该算法定义如下.

算法3. CheckBasicType.

Input: t;

Output: T.

1.    begin

2.    ResultList=null; //初始化结果集

3.    aList= TR3(t); //判断输入项是否为带标签的数据元

4.    if (aList!= null)

     for aList中的每个t' :{l:T}:

       if B={l:T}∈数据元集合输出t:B;

       else输出受阻;

5.   else继续执行步骤6

6.   遍历枚举类型集合中的每一个P, 若t:P, 输出t:P; 否则, 继续执行步骤8

7.    bList=TR6(t); //判断输入项是否为值域表达式类型

8.    if (bList!=null)输出bList中的t:E, else输出受阻

9.    end

根据上述算法的逻辑和文献[19]中TR3, TR6检测算法的定义, 其时间复杂度O_T2为O(C×H×K×N), O(N×n), O(C×H×K×N×n)中的最高者, 空间复杂度O_S2为O(n), 其中, n为构成输入项t的所有分项t_i的个数.即, n是输入相关变量.

(3) 子算法3

CheckComposedType为数据元目录检查算法, 该算法通过对圆括号中的每一个以符号“, ”间隔的项进行判定(基本类型、枚举类型或值域表达式类型), 给出这些类型所构造的数据元目录.该算法定义如下.

算法4. CheckComposedType.

Input: t;

Output: T.

1.    begin

2.    ResultList=null; //初始化结果集

3.    ResultList=TR4(t); //判断输入项是否为数据元目录

4.    if (ResultList!=null)输出ResultList中的t:T else继续执行步骤5

5.    ResultList=TR5(t); //判断输入项是否为枚举类型构造的数据元目录

6.    if (ResultList!=null)输出ResultList中的t:T else继续执行步骤7

7.    ResultList=TR7(t); //判断输入项是否为值域表达式类型构造的数据元目录

8.    if (ResultList!=null)输出ResultList中的t:T else输出受阻

9.    end

根据上述算法的逻辑和文献[19]中TR4, TR5, TR7检测算法的定义, 其时间复杂度O_T3为O(C×H×K×n), O(C× H×K×N×n), O(N×n), O(C×H×K×N²×n)中的最高者, 空间复杂度O_S3为O(n), O(2n), O(1)中的最高者, 其中, n为构成输入项t的所有分项t_i的个数.

上述CheckType算法主要用于给定一个项t, 判定其所属的类型为T.该算法的时间复杂度相当于O(C×H× K×N²×n), 空间复杂度相当于O(2n), 其中, n的含义同上.此外, 数据元目录之间的关系也是检查的内容, 即:给定两个数据元目录T₁和T₂, 判定它们之间存在什么类型关系(或给定T₁, T₂和一个类型关系R判定该关系是否满足).本文通过算法CheckRelation实现这一功能, 该算法在所有关系类类型规则检查算法^[19]的基础上定义.为便于描述其时间和空间复杂度, 模型中的数据元、数据元目录个数仍记为N, M, 数据元目录之间关系的类型规则个数记为L.研究报告^[19]中标明模型中关系类类型规则TR8~TR13同名检查算法的时间和空间复杂度. CheckRelation算法具体流程如下.

算法5. CheckRelation.

Input: T₁, T₂, o;

Output: R.

1.    begin

2.    result=false; //初始化结果, 假定为不成立

3.    R=null //可能的关系

4.    if ((T₁, T₂, R)形如TR9的分母); //若符合类型关联规则的分母

  a)    R=类型关联; result=TR9(T₁, T₂, R)

5.    else if ((T₁, T₂, o)形如TR10的分母); //若符合对象关联规则的分母

  a)    R=对象关联; result=TR10(T₁, T₂, o)

6.    else if ((T₁, T₂, o)形如TR11的分母); //若符合枚举关联规则的分母

  a)    R=枚举关联; result=TR11(T₁, T₂, o)

7.    else if ((T₁, T₂, o)形如TR12的分母); //若符合值域类型关联规则的分母

  a)    R=值域类型关联; result=TR12(T₁, T₂, o)

8.    if (result==true)输出R //存在关系R

9.    else输出R=null //数据元目录无关联

10.   end

根据上述算法的逻辑和文献[19]中TR9~TR12检测算法的定义, 以及项的类型判定算法的效率分析, 其时间复杂度相当于O(N×2M×N²×L+C×H×K×N²×n), 空间复杂度为O(2N+L), 其中, N的含义同上, 表示数据元个数.

最后, 本文给出数据元目录序列正确性的判定算法, 该算法通过给定的数据元目录序列及其应满足的类型关系集合, 判定类型关系集合中的每个类型关系R_i是否满足.其具体流程如下.

算法6. CheckCorrectness.

Input: $ {({T_1}, ..., {T_m})_{\{ {R_1}, ..., {R_k}\} }}$;

Output: boolean.

1.    begin

2.    correctFlag=false; //初始化结果, 假定为不正确

3.   遍历{R₁, …, R_k}, 对每一个R_i

4.   获取R_i中的T₁, T₂, o //此处o为对象关联关系中的对象

5.    if ({T₁; T₂}⊆{T₁; …; T_m}) //类型关系相关的数据元目录存在

  a)    R=CheckRelation(T₁, T₂, o)

  b)    if (R==R_i)correctFlag=true

  c)    else correctFlag=false

6.    else correctFlag=false

7.    if (correctFlag==true)输出正确

8.    else输出不正确

9.    end

根据上述算法的逻辑和CheckRelation算法的效率分析, 其时间复杂度为O((N×2M×N²×L+C×H×K×N²×n)× m×k), 空间复杂度为O(2N+L+m+k), 其中, m, k和n分别表示数据元目录序列长度、应满足关系集合长度以及构成算法中项o的所有成员个数, 即, m, k和n是输入相关变量.

容易看出:数据元目录之间关系和数据元目录序列正确性的判定问题最终都可以归结为判定Γ|-t:T是否成立的问题上, 并且上述算法总是能够终止.此外, 算法的时间复杂度为三次多项式复杂, 空间复杂度为一次多项式复杂.DDML语言、DDMM方法及其类型检查算法合起来构成DDMS(domain data modelling system)系统.关于DDMS系统的可判定性证明, 即, 其类型检查算法(CheckType, CheckRelation和CheckCorrectness算法)的可靠性、完备性以及算法的可终止性的详细证明, 见文献[1].

本文在上述理论与算法的基础上, 设计并实现了DDMS原型系统工具, 其总体构造如图 2所示.

DDMS分为3个部分:领域数据需求分析、领域数据建模以及领域数据模型验证.该系统逐层创建领域各层的数据类型, 同时, 将需求中需要验证的性质作为验证目标输入系统.在验证过程中, 系统首先对目标性质的每个逻辑单元进行判定, 并最终计算出表示目标性质的命题是否成立, 从而判断所创建的领域数据模型是否满足需求.

DDML语言及DDMM方法可以为一般行业制定其信息系统基本数据规范并且进行验证.通过对实际行业需求和数据特点的分析, 逐层生成数据模型和类型规则, 形成领域数据模型, 并验证这一数据模型的正确性.

3 殡葬领域数据建模案例

作为一个案例研究, 本文采用DDMS原型系统工具构建殡葬领域数据模型, 并验证该模型.

3.1 殡葬领域数据需求分析

本案例的需求为制定民政部殡葬管理与服务信息系统的基本数据规范(以下称简称数据规范), 并确保其满足业务需求.该数据规范旨在为殡葬机构对其业务数据进行实时动态查询、维护、汇总和推送, 为民政主管部门实时动态了解所辖地区殡葬业务运行情况、动态统计分析等提供基本数据支持.殡葬管理与服务信息系统主要包括殡葬业务管理和殡葬业务服务, 其中, 殡葬业务服务系统主要提供殡仪业务、安放/安葬业务、祭祀/祭扫业务等服务.数据规范是殡葬管理与服务信息系统建设的前提和基础.

数据规范的编制内容, 源于本行业领域专家的知识和实际业务中的数据需求.数据规范不仅应覆盖一般实体数据, 还要体现不同实体数据之间的关系.一般实体数据是指殡葬管理与服务中涉及到的实体的信息, 如殡葬机构、员工、殡葬设施/设备/用品以及殡葬业务相关信息.而实体数据之间的关系则是指实体之间是否从属、是否相关等信息.此外, 对于一个整体业务服务, 数据规范还应满足业务节点中的数据前后一致.

根据以上要求, 编制数据规范的需求分为两部分:第1部分为实体数据需求; 第2部分为业务连贯性需求.本文对原始需求采用表格的方式记录(见附录1, 完整需求见文献[19]), 通过需求分析, 进一步刻画为需求图.

3.1.1 实体数据需求

实体数据主要刻画实体属性和实体从属.实体属性指每个实体应具备的基本属性, 用于描述一个实体由哪些元素构成.此类需求可分析为一个数据元目录由哪些数据元聚合而成.实体从属用于描述一个实体从属于哪些实体.例如, 某个实体B从属于A, 此类需求可分析为数据元目录A与数据元目录B之间的类型关联, 其中, 所关联的数据元为某一个实体的标识, 例如:员工从属于机构, 则员工信息中有机构标识的属性; 机构有设施, 则设施信息中有机构标识的属性.

本文采用图形化设计工具(如UML)对此进行描述.鉴于该部分的内容较多, 限于篇幅, 本文以图 3为例展示机构信息、年检信息以及殡仪业务信息等数据元目录的构成及其关系, 如图 3所示.类似地, 以图 4为例展示数据元目录之间关系, 如图 4所示.更多详细需求, 见文献[19].

3.1.2 业务连贯性需求

根据本应用背景, 殡葬管理与服务信息系统的业务包括3类:一是殡仪服务; 二是安放/安葬服务; 三是祭祀/祭扫服务.3类业务均有各自的业务流程, 每个业务流程通常由多个分支组成, 并且每个分支上存在多个节点.要求这3个业务流程均能满足其所有分支上的节点所需数据存在, 并且要求前后节点数据之间能够关联.例如:在殡仪业务流程中, 办理遗体接运、保存、守灵、防腐、整容以及火化、取灰等一系列节点中, 前后节点的机构、设备、设施或逝者信息应统一.

因此, 业务连贯性需求主要描述每类业务流程的各个分支需要哪些数据以及前后节点的数据之间是否有联系, 即, 每类业务的各个分支中应满足一系列数据元目录序列以及数据元目录之间的关系.本文采用图形化建模工具, 如BPMN(business process modelling notation), 详细描述.其中, 以殡仪业务为例, 其业务流程中所需要的数据如图 5所示.

图 5中:虚线表示该服务节点上所需输入的数据和所要输出的数据信息; 实线表示业务流程的顺序.图中的开始节点到结束节点形成一个业务分支, 每个业务分支由多个服务节点组成.以图 5为例, 殡仪业务流程包括10个服务节点, 其中, “遗体接运”服务又可以划分为“遗体出车”“国际运尸”和“遗体异地运输”这3个分支, 因此, 殡仪业务流程包括从开始节点到结束节点的3条业务分支.若依次记录服务节点为S₁, S₂, S₃, S₄, S₅, S₆, S₇, S₈, S₉, S₁₀(其中, $ {S_2} = S_2^1|S_2^2|S_2^3$表示三者选一), 则殡仪业务连贯性可以视为每个S_i需要的输入/输出数据是否定义以及它们之间关系是否得到满足.图 5中, 每个业务分支的不同服务节点都以同一个“机构”数据与“逝者/使用者”数据作为输入, 表示该分支中“机构标识”与“逝者/使用者标识”前后一致.类似地, 其他两个服务的业务流程的图形化展示见文献[19].

将UML和BPMN刻画的需求图进行导出, 可以转化为程序可处理的XML文件, 通过解析这些XML文件, 可以得到响应的实体数据需求点和业务连贯性需求点.关于如何导出以及如何解析的方法及理论, 限于篇幅, 本文不再赘述.

3.2 殡葬领域数据建模

为满足上述需求, DDMS原型系统采用DDML语言及DDMM方法, 对殡葬领域数据进行建模.建模包括𝒦₁原子类型及约束, 𝒦₂数据元、枚举类型、值域表达式类型以及𝒦₃数据元目录及其关系.

3.2.1 原子类型及约束

原子类型是殡葬行业数据类型的基础, 它包括, string, integer, float, date, datetime, boolean, binary, Digit, Alphabet和Nat等10种类型, 分别编号为A₁~A₁₀.它们构成数据模型中𝒦₁层, 其类型总数为10个.为方便在实际规范中引用, 在应用中采用以下更为直观的约束表达式形式.

由第2.1节中关于类型的定义, 约束表达式〈constraint〉用于限定某一类对象, 其形式定义为

constraint::=number|…number|number₁…number₂|n number|n…number|an number|,

其中, number:Nat, number₁:Nat, number₂:Nat, a as Alphabeta(||Alphabet||={a, …, z, A, …, Z}), n as Digit(||Digit||={0, 1, …, 9}), an as(Alphabeta+Digit)^*.as表示类型归属, 归属也是一种类型^[1].容易看出, 每个约束表达式相当于DDML中约束的一个实例.表 1给出了应用中的约束形式及其在DDML中对应的约束表达式.

3.2.2 数据元

由第2.7节中定义2, 数据元由原子类型加上标签和约束表达式构造而成, 其中, 约束表达式可以为空.

应用中的数据元集合记为{B₁, …, B_n}, 其中, B_i=l_i:A_j with 〈constraint_i〉(0≤i≤n).为满足附录1和文献[19]中记述的需求, 以下举例给出本文创建和表述数据元的方式.

例  1:string with 〈an16〉表示长度为16的英文字母加数字符号串类型.应用中, 机构标识B₁满足该约束, 其标识为“instId”, 因此有B₁=instId:A₁ with 〈an16〉.

例  2:表 2为本文定义数据元的方式, 其中, 表头的“数据元编号”表示第i个数据元B_i; 第1行中的标签“instCode”和约束〈an18〉表示数据元B₁₂(“统一信用代码”)是18位字母与数字组合的字符串类型, 因此, B₁₂=A₁ with 〈an18〉; 第2行中的标签“useLimit”和约束〈n…3〉, 表示数据元B₄₈(“使用年限”)是3位数字以内的整数类型, 因此有B₄₈=A₂ with 〈n…3〉.采用这一方式, DDMS原型系统生成了《原子类型基本类型定义》^[19], 它给出了殡葬行业数据规范需要的所有数据元的定义, 它们构成数据模型中的𝒦₂层, 其类型总数为549个.

3.2.3 数据元目录

由第2.7节中定义3, 数据元目录是由数据元聚合而成的类型, 或者由某个枚举类型或值域表达式构造而成的类型.

应用中的数据元目录集合记为{T₁, …, T_x}, 其中, T_j=B_j1×…×B_jk(1≤j≤x, 1≤k≤n).B_jk可以是数据元, 也可以是枚举类型或值域表达式类型.

设有如下原子类型或数据元的项:

a, b, y, m, d, x:A₈, b₁₁:B₁₁, b₁₂:B₁₂, b₁₃:B₁₃, b₂₇₄:B₂₇₄, b₂₈₃:B₂₈₃, b₃₀₈:B_308,

则根据第2.5节中值域表达式的定义, 可以构造本应用中的值域表达式, 其定义如下:

range_exp::=aaaaaaaaaaaa|xxxx-aaaaaaaa-bbb|b₁₁_b₁₃_xxxxxx|

‘S’_b₁₁_b₁₂_xxxxxx|‘C’_b₁₁_b₁₂_xxxxxxxx|‘E’_b₁₁_yyy_xxxxxx|

‘IM’_b₁₁_b₁₂_b₂₇₄_xxxxxx|‘EQ’_b₁₁_b₁₂_b₂₈₃_xxxxxx|

‘Y’_b₁₁_b₁₂_b₃₀₈_xxxxxx|‘F’_b₁₁_b₁₂_yyymmdd_xxxxxx|

‘B’_b₁₁_b₁₂_yyymmdd_xxxxxx|‘T’_b₁₁_b₁₂_xxxxxxxx|

‘D’_b₁₁_b₁₂_yyymmdd_xxxxxx.

若对每个表达式分别记为E₁, E₂, …, E₁₃, 则本应用中值域表达式类型有13个, 其对应的数据元, 见表 3, 其中, 第3列“构成元素”表示该表达式是将这些构成元素以字符“_”(或“-”)分隔并串连而成的.

在DDMS原型系统生成的原子类型基本类型定义^[19]中, 给出了殡葬行业数据规范需要的所有枚举类型及值域表达式类型的定义, 并在值域中列出了每个类型的项可能的取值或对应的值域表达式编号.

为满足附录1和文献[19]中记述的需求, 本文以电子表格及其宏定义程序的方式给出应用中创建的数据元目录.

例3:表 4中, 每个数据元目录为电子表格中的一个表单, 该表单有纵向表头和横向表头.其中, 纵向表头中的类型名称为数据元目录的名称, 类型编号为数据元目录的编号, 浅灰色表头下面每行表示该数据元目录由哪些数据元构成以及这些数据元又由哪些原子类型加约束构成.将横纵信息结合, 可在TypeExp中计算出该数据元目录的类型表达式.例如:数据元目录机构基本信息T₂由20余种数据元聚合而成, 包括机构标识类B₁, …, 机构类型类B₁₃, …, 服务范围B₉₃等.

采用这一方式, DDMS原型系统生成了复合类型定义^[19], 它给出了殡葬行业数据规范需要的所有数据元目录, 其中有76个由基本类型聚合而成数据元目录, 106个由枚举类型或值域表达式类型构造而成的数据元目录.它们构成数据模型中的𝒦₃层, 其数据元目录总数为182个.

3.2.4 类型关系及类型规则

领域数据模型中的各层类型之间存在一定的关系, 类型关系是指每层类型之间以及某些层内类型之间的关系.类型关系既可以采用类型表达式, 也可以采用类型规则描述.若采用类型表达式, 应用中的类型关系可以写为

R₁(T₁₁, …, T_1i), …, R_k(T_k1, …, T_kj),

其中, {T₁₁, …, T_1i}⊆{T₁, …, T_m}, ..., {T_k1, …, T_kj}⊆{T₁, …, T_x}.

为类型关系描述直观和算法处理方便, 本文采用类型规则描述, 并对其进行如下分类.

1)   在第2层与第1层之间, 约束关系的类型规则;

2)   在第3层与第2层之间, 聚合关系的类型规则;

3)   在第3层数据元目录之间的一般关联、枚举关联和值域表达式关联等关系的类型规则.

根据第2.5节定义的类型规则, 在本应用案例中有如下类型规则.

(1) 约束关系的类型规则

数据元由原子类型加约束构成, 因此, 原子类型与数据元之间存在约束关联.例如, 表 4中记录了数据元机构

标识(B₁)的构成关系(A₁)和格式要求(〈an16〉), 说明原子类型A₁和数据元B₁之间存在约束关系, 即${{A}_{1}}\xrightarrow{\langle an16\rangle }{{B}_{1}} $.为便于程序处理, 将类型的下标均写为正常序号, 因此, 表 4中A₁=A₁, B₁=B₁.

本应用中的约束关系的类型规则总共有480个.

(2) 聚合关系的类型规则

数据元目录由数据元聚合而成, 因此数据元与数据元目录之间存在聚合关系.例如, 表 4中记录了数据元目录(T₂)与20多个数据元(B₁, …, B₂₂, …, B₉₃), 并在“TR分子”和“TR分母”中给出了当前数据元目录由数据元聚合而成的类型规则, 如下所示:

$ \begin{align} & \frac{T={{B}_{1}}\times ...\times {{B}_{13}}\times ...\times {{B}_{22}}\times {{B}_{93}}\text{ }}{{{B}_{1}}\xrightarrow{◇}T或T.1\xrightarrow{◇}T},...,\frac{T={{B}_{1}}\times ...\times {{B}_{13}}\times ...\times {{B}_{22}}\times {{B}_{93}}\text{ }}{{{B}_{13}}\xrightarrow{◇}或T.13\xrightarrow{◇}\text{ }T},..., \\ & \frac{T={{B}_{1}}\times ...\times {{B}_{13}}\times ...\times {{B}_{22}}\times {{B}_{93}}\text{ }}{{{B}_{22}}\xrightarrow{◇}T或T.18\xrightarrow{◇}T},...,\frac{T={{B}_{1}}\times ...\times {{B}_{13}}\times ...\times {{B}_{22}}\times {{B}_{93}}\text{ }}{{{B}_{93}}\xrightarrow{◇}或T.21\xrightarrow{◇}T}. \\ \end{align} $

本应用中的聚合关系的类型规则有706个.

(3) 一般关联

一般关联指DDML语言的类型关联和对象关联.在本应用中, 数据元目录T₁₅和数据元目录T₂的元组中都有数据元B₁(见文献[19]), 因此, 它们之间存在类型关联, 其类型规则如下所示:

$ \frac{\text{ }{{B}_{1}}={{T}_{15}}.2,{{B}_{1}}={{T}_{2}}.1}{{{T}_{15}}\overset{{{B}_{1}}}{\longleftrightarrow}{{T}_{2}}} $

并且, 对于对象instId:B₁, 存在它们之间的对象关联, 其类型规则如下所示:

$ \frac{instId:{{B}_{1}},{{B}_{1}}={{T}_{15}}.2,{{B}_{1}}={{T}_{2}}.1}{{{T}_{15}}\overset{instId}{\longleftrightarrow}{{T}_{2}}} $

本应用中的类型关联有150个.

(4) 枚举关联

枚举关联是指枚举类型构造的数据元目录和引用该枚举类型的数据元目录之间的关联.在本文规范中, 机构设施信息的数据元目录类型为T₁₄, 其第9个元组的类型为数据元B₂₇₉(“设施状态”), 它的值域通过列举枚举类型T₁₂₄(“设施状态类别”)值的方式给出.因此, 类型T₁₄和类型T₁₂₄满足〈〈enum〉〉关联, 其类型规则如下所示:

$ \frac{''01'':{{B}_{279}},''02'':{{B}_{279}},''03'':{{B}_{279}},{{T}_{14}}.j={{B}_{279}},{{T}_{115}}=\{{{B}_{279}}\}}{{{T}_{14}}\xrightarrow{\{''01'',''02'',''03''\}/\langle \langle enum\rangle \rangle }{{T}_{124}}} $

本应用中, 枚举关联有100个.

(5) 值域表达式关联

值域关联是指值域表达式类型构造的数据元目录和引用该值域表达式类型的数据元目录之间的关联.结合表 3和表 4, 机构基本信息的数据元目录类型T₂的第一元组类型为数据元B₁(“机构标识”), 其值域由值域表达式E₂给出.因此, 数据元目录T₂与值域表达式构造的数据元目录T₁₇₁之间存在值域关联, 其类型规则如下所示:

$ \frac{t:{{E}_{2}},{{T}_{171}}=\{{{E}_{2}}\},{{T}_{2}}.j={{E}_{2}}\text{ }}{{{T}_{2}}\xrightarrow{t/\langle \langle range\rangle \rangle }{{T}_{171}}} $

本应用中, 值域关联有156个.

3.2.5 应用环境

根据DDML语言中环境的定义, 殡葬领域数据模型中的应用环境定义如下.

约定.将𝒦₁层的原子类型称为初始应用环境, 记为Γ₁.领域数据模型中的所有类型的集合称为应用环境, 记为Γ.

设Γ₂表示数据元, Γ₃表示数据元目录, 则根据定义8, Γ=Γ₁→Γ₂→Γ₃.本文所要验证的性质就是在该应用环境Γ下的性质.

3.3 殡葬领域数据模型验证

本节给出领域数据模型需要验证的性质, 并采用DDMS原型系统对所创建模型进行验证.其主要方法是将数据模型所期望的性质P, 根据第3.1节中需求图的描述及其的解析, 转化为判定一组数据元目录序列是否正确, 并利用DDMM中的数据元目录序列正确性判定算法(CheckCorectness), 验证P是否成立.

根据文献[19]中数据元目录的编号及其构成以及第3节中对业务流程中数据需求的分析, 可以将每个业务流程中需要的数据视为该业务流程需要的数据元目录序列, 将前后服务节点数据的一致性要求视为相应服务节点的数据元目录之间应满足对象关联.假定3种业务流程应该满足的性质分别记为P₁, P₂和P₃, 分别表示殡仪业务流程、安放/安葬业务流程、祭祀/祭扫业务流程所需数据元目录序列及其应满足关系集合.

为模拟业务连贯性需求, 对每个业务分支中每个服务节点的数据需求进行刻画, 形成表 5的数据元目录序列及其类型关系集合.

表 5中每一行数据元目录序列及其关系集合所表达的具体含义见表 6.

篇幅所限, 表 6的详细内容请见文献[19]中验证关系含义.

结合上述表 5和表 6, 殡仪业务流程连贯性需求P₁可以写为如下形式:

P₁=R_SEQ1∧ (R_SEQ21∨ R_SEQ22∨ R_SEQ23)∧R_SEQ3∧R_SEQ4∧ R_SEQ5∧R_SEQ6∧R_SEQ7∧R_SEQ8∧R_SEQ9∧R_SEQ10.

类似地, 安葬安葬业务流程和祭祀祭扫业务流程的连贯性需求P₂和P₃可以写为如下形式:

P₂=(R_SEQ11∧ R_SEQ12∧R_SEQ13∧R_SEQ14∧R_SEQ15∧R_SEQ16)∨ (R_SEQ19∧ R_SEQ18∧R_SEQ17)∨ R_SEQ20;

P₃=R_SEQ31∨ R_SEQ32∨ R_SEQ33.

如图 2所示:在验证部分, 将P₁, P₂, P₃对应的数据元目录序列及其关系集合作为输入, 采用CheckCorrectness算法判定其是否成立.若有一项不符合, 则领域数据建模过程存在错误, 即不能满足需求.经过实际验证.领域数据模型及其验证相关的结果如图 6所示.

图 6(c)列出了P₁, P₂, P₃等性质的验证结果.根据表 5的定义, 它们对应的性质公式待验证的单元个数分别为12, 10和3, 待验证数据元目录关系个数分别为45, 36和10.容易看出, 对3个性质验证通过的关系个数与待验证关系个数相同.因此, 本文所创建的数据模型能够满足当前业务连贯性需求.此外, 根据图 6(a)和图 6(b)中的统计, 殡葬领域数据模型中定义的原子类型、数据元、数据元目录以及数据元目录之间关系的个数分别为C=10, N=549, M=184和L=150个.根据表 5和表 6, 验证性质P₁, P₂, P₃所涉及的数据元、数据元目录和数据元目录之间关系的个数分别为N_r=549, M_r=76和L_r=84.由于M_r < M, L_r < L, 即, 本应用定义的数据元、数据元目录及其关系的个数要大于验证性质P₁, P₂, P₃实际所用到的相关数据元、数据元目录及其关系总数, 因此, 当前的领域数据模型还可以用于满足其他可能的需求.由于其需求分析方法和验证方法类似, 本文不再赘述.

上述验证的基础是对任意给定的项t, 能够判定其所属的类型T.为此, 通过一个实际案例, 以类型规则推导树的形式给出DDMS原型系统判定G|-t:T的过程.对于任意输入项t, 调用CheckType(t)算法, 将t逐个分解, 利用模型中已定义的类型规则及其检查算法, 判定各个分项t_i的类型, 并最终判定t所属的类型.本案例输入的项t的形式如下:

$ \begin{array}{l} t = (\{ facilityId = IM\_010010\_101820091890201001\_03\_000301\} , \\ {\rm{ }}\{ instId = 010010\_01\_000014\} , \{ facilitiesName = 35号守灵室\} , \{ resourceType = 06\} , \\ {\rm{ }}\{ buildArea = 25.0\} , \{ capacity = 2\} , \{ useDate = 2017 - 04 - 05\} , \{ stopDate = 2027 - 04 - 05\} , \\ {\rm{ }}\{ status = 02\} , \{ facilitiesDesc = 守灵室用于为逝者守灵\} ). \end{array} $

容易看出, t有10个分项, 分别记为t₁, …, t₁₀, 则通过判定每一个t_i(1≤i≤10), 可得出t:T₁₄的判定结果, 如以下类型规则推导树所示:

$ \frac{\begin{array}{l} {t_1}:{B_{272}}, {t_2}:{B_1}, {t_3}:{B_{273}}, {t_4}:{B_{274}}, {t_5}:{B_{275}}, {t_6}:{B_{276}}, {t_7}:{B_{277}}, {t_8}:{B_{278}}, {t_9}:{B_{279}}, {t_{10}}:{B_{280}}, \\ t = ({t_1}, {t_2}, {t_3}, {t_4}, {t_5}, {t_6}, {t_7}, {t_8}, {t_9}, {t_{10}}), {\rm{ }}\\ {T_{14}} = {B_{272}} \times {B_1} \times {B_{273}} \times {B_{274}} \times {B_{275}} \times {B_{276}} \times {B_{277}} \times {B_{278}} \times {B_{279}} \times {B_{280}} \end{array}}{{t:{T_{14}}}}({\rm{TR}}4). $

限于篇幅, 判定每一个t_i的类型规则推导树请详见附录2验证过程例示.

4 结论

本文在理论和应用上的主要贡献是提出了一种基于类型理论的领域数据建模语言DDML、领域数据建模方法DDMM及其验证方法和领域数据建模工具原型系统DDMS, 适用于一般领域的数据建模和验证; 提出了数据元目录序列正确性验证方法, 从而可以验证所创建的领域数据模型是否满足业务需求; 为殡葬行业制定行业数据规范并验证了该规范的正确性, 完成了大规模行业数据建模及其验证案例, 说明了方法的有效性.

附录1
附录2

验证过程例示:输入项t, 判断其类型T.

假设输入项t为如下形式:

验证过程:

系统通过CheckType(t)进行验证.这一过程中, 首先调用CheckComposedType(t)方法的TR4(t)分支.再根据t的格式对构成t的每个分项调用TR3(t_i)(i=10).

下面给出每个t_i的判定过程:

(1) t₁={faclityId=IM_010010_101820091890201001_03_000301}的判定树如下:

$ \frac{{l = facilityId, \frac{\begin{array}{l} {t_{11}} = IM:{A_1}, \frac{{\frac{{\frac{{\frac{{0:{A_8}, 1:{A_8}}}{{0:{A_1}, 1:{A_1}}}{\rm{ }}({\rm{TR}}2)}}{{010010:{A_1}}}({\rm{TR}}1), 010010满足\langle n6\rangle }}{{010010:{A_1}{\rm{ with }}\langle n6\rangle , {B_{11}} = {A_{\rm{1}}}{\rm{ with }}\langle n6\rangle }}({\rm{TR}}2)}}{{{t_{12}} = 010010:{B_{11}}}}, \\ \\ \frac{{\frac{{\frac{{\frac{{0:{A_8}, 1:{A_8}, 2:{A_8}, 8:{A_8}, 9:{A_8}}}{{0:{A_1}, 1:{A_1}, 2:{A_1}, 8:{A_1}, 9:{A_1}}}{\rm{ }}({\rm{TR2}})}}{{101008091890201001:{A_1}{\rm{ }}}}({\rm{TR1}}), 101008091890201001满足\langle n18\rangle {\rm{ }}}}{{101008091890201001:{A_{\rm{1}}}{\rm{ with }}\langle n18\rangle }}({\rm{TR}}2), {B_{12}} = {A_{\rm{1}}}{\rm{ with }}\langle n18\rangle }}{{{t_{13}} = 101008091890201001:{B_{12}}}}{\rm{ }}({\rm{TR}}2), \\ \\ \frac{{\frac{{\frac{{0:{A_1}, 6:{A_1}}}{{06:{A_1}}}({\rm{TR1}}), 06{\rm{ }}满足\langle ...2\rangle }}{{06:{A_{\rm{1}}}{\rm{ with }}\langle ...2\rangle }}({\rm{TR2}}), {B_{274}} = {A_1}{\rm{ with }}\langle ...2\rangle }}{{{t_{14}} = 06:{B_{274}}}}{\rm{, }}\frac{{\frac{{0:{A_1}, 1:{A_1}, 3:{A_1}}}{{000301:{A_1}}}({\rm{TR}}1), 000301{\rm{ }}满足\langle n6\rangle }}{{{t_{15}} = 000301:{A_{\rm{1}}}{\rm{ with }}\langle n6\rangle }}{\rm{ }}({\rm{TR}}2){\rm{ }} \end{array}}{{range\_{\rm{exp}}({t_{11}}, {t_{12}}, {t_{13}}, {t_{14}}, {t_{15}}):{E_7}, IM\_010010\_101820091890201001\_03\_000301满足\langle an38\rangle }}({\rm{TR}}6, {\rm{TR}}2), {B_{272}} = {E_7}, {B_{272}} = \{ facilityId:{A_1}{\rm{ with }}\langle an38\rangle {\rm{ }}}}{{\{ facilityId = IM\_010010\_101820091890201001\_03\_000301\} :{B_{272}}}}{\rm{ }}({\rm{TR}}3). $

其中, range_exp(t₁₁, t₁₂, t₁₃, t₁₄, t₁₅)为将t₁₁~t₁₅以字符“_”分隔并串连而成的字符串.

(2) t₂={instId=010010_01_000014}:

$ \frac{{l = instId, \frac{\begin{array}{l} \frac{{\frac{{\frac{{\frac{{0:{A_8}, 1:{A_8}}}{{0:{A_1}, 1:{A_1}}}({\rm{TR}}2)}}{{{\rm{ }}010010:{A_1}{\rm{ }}}}({\rm{TR}}1), 010010满足\langle n6\rangle }}{{010010:{A_1}{\rm{ with }}\langle n6\rangle }}({\rm{TR}}2), {B_{11}} = {A_1}{\rm{ with }}\langle n6\rangle }}{{{t_{21}} = 010010:{B_{11}}}}, \\ \\ \frac{{\frac{{\frac{{0:{A_1}, 1:{A_1}}}{{01:{A_1}}}({\rm{TR1}}), 01{\rm{ }}满足\langle ...2\rangle {\rm{ }}}}{{01:{A_1}{\rm{ with }}\langle ...2\rangle }}({\rm{TR2}}), {B_{13}} = {A_{\rm{1}}}{\rm{ with }}\langle ...2\rangle }}{{{t_{22}} = 01:{B_{13}}}}{\rm{, }}\\ \\ \frac{{\frac{{0:{A_1}, 1:{A_1}, 4:{A_1}}}{{000014:{A_1}}}({\rm{TR}}1), 000014满足\langle n6\rangle }}{{{t_{15}} = 000014:{A_1}{\rm{ with }}\langle n6\rangle }}({\rm{TR2)}} \end{array}}{{range\_\exp ({t_{21}}, {t_{22}}, {t_{23}}):{E_3}, 010010\_01\_000014满足\langle an16\rangle }}({\rm{TR}}6), {B_1} = {E_3}, {B_1} = \{ instId:{A_1}{\rm{ with }}\langle an16\rangle \} {\rm{ }}}}{{\{ instId = 010010\_01\_000014\} :{B_1}}}({\rm{TR}}3). $

(3) t₁={facilitiesName=35号守灵室}:

$ \frac{{l = facilitiesName, \frac{{{t_{31}} = 35号守灵室:{A_1}, {t_{31}}满足\langle ...64\rangle }}{{{t_{31}}:{A_1}{\rm{ with }}\langle ...64\rangle }}{\rm{ }}({\rm{TR}}2), {B_{273}} = \{ facilitiesName:{A_1}{\rm{ with }}\langle ...64\rangle \} }}{{\{ facilitiesName = 35号守灵室\} :{B_{273}}}}({\rm{TR3}}). $

(4) t₄={resourceType=06}:

$ \frac{{l = resourceType, \frac{{{t_{41}} = 06:{A_1}({\rm{TR1)}}, {t_{41}}满足\langle n2\rangle }}{{{t_{91}}:{A_{\rm{1}}}{\rm{ with }}\langle n2\rangle }}({\rm{TR}}2), {B_{274}} = \{ resourceType:{A_{\rm{1}}}{\rm{ with }}\langle n2\rangle \} }}{{\{ resourceType = 06\} :{B_{274}}}}{\rm{(TR3)}}. $

(5) t₅={bulidArea=25.0}:

$ \frac{{l = buildArea, {t_{51}} = 25.0:{A_3}({\rm{TR2}}), {B_{275}} = \{ buildArea:{A_3}{\rm{ }}\} }}{{\{ buildArea = 25.0\} :{B_{275}}}}({\rm{TR3)}}. $

(6) t₆={capacity=2}:

$ \frac{{l = capacity, {t_{61}} = 2:{A_2}({\rm{TR2}}), {B_{276}} = \{ capacity:{A_2}{\rm{ }}\} }}{{\{ capacity = 2\} :{B_{276}}}}({\rm{TR}}3). $

(7) t₇={useDate=2017-0405}:

$ \frac{{l = useDate, \frac{{\frac{{{y_1} = 2, {y_2} = 0, {y_3} = 1, {y_4} = 7, {m_1} = 0, {m_2} = 4, {d_1} = 0, {d_2} = 5:{A_8}}}{{{t_{71}} = {y_1}{y_2}{y_3}{y_4} - {m_1}{m_2} - {d_1}{d_2} = 2017 - 04 - 05:{A_4}}}{\rm{ }}({\rm{TR}}1), {t_{71}}满足\langle 10\rangle }}{{{t_{71}}:{A_4}{\rm{ with }}\langle 10\rangle }}({\rm{TR}}2), {B_{277}} = \{ useDate:{A_4}{\rm{ with }}\langle 10\rangle \} }}{{\{ useDate = 2017 - 04 - 05\} :{B_{277}}}}({\rm{TR3}}). $

(8) t₈={stopDate=2017-0405}:

$ \frac{{l = stopDate, \frac{{\frac{{{y_1} = 2, {y_2} = 0, {y_3} = 2, {y_4} = 7, {m_1} = 0, {m_2} = 4, {d_1} = 0, {d_2} = 5:{A_8}}}{{{t_{81}} = {y_1}{y_2}{y_3}{y_4} - {m_1}{m_2} - {d_1}{d_2} = 2027 - 04 - 05:{A_4}}}{\rm{(TR}}1), {t_{81}}满足\langle 10\rangle }}{{{t_{81}}:{A_4}{\rm{ with }}\langle 10\rangle }}({\rm{TR}}2), {B_{278}} = \{ stopDate:{A_4}{\rm{ with }}\langle 10\rangle \} }}{{\{ stopDate = 2027 - 04 - 05\} :{B_{278}}}}({\rm{TR}}3). $

(9) t₉={status=02}:

$ \frac{{l = status, \frac{{{t_{91}} = 02:{A_1}(TR1), {t_{91}}满足\langle ...2\rangle }}{{{t_{91}}:{A_{\rm{1}}}{\rm{ with }}\langle ...2\rangle }}({\rm{TR}}2), {B_{279}} = \{ status:{A_1}{\rm{ with }}\langle ...2\rangle \} }}{{\{ status = 02\} :{B_{279}}}}({\rm{TR}}3). $

(10) t₁₀={facilitiesDesc=守灵室用于为逝者守灵}:

$ \frac{{l = facilitiesDesc, \frac{{{t_{101}} = 守灵室用于为逝者守灵:{A_1}, {t_{101}}满足\langle ...1024\rangle }}{{{t_{101}}:{A_{\rm{1}}}{\rm{ with }}\langle ...1024\rangle }}({\rm{TR2}}), {B_{280}} = \{ facilitiesDesc:{A_1}{\rm{ with }}\langle ...1024\rangle \} }}{{\{ facilitiesDesc = 守灵室用于为逝者守灵\} :{B_{280}}}}({\rm{TR}}3). $

最后, 根据t=(t₁, t₂, t₃, t₄, t₅, t₆, t₇, t₈, t₉, t₁₀), 有如下判定:

$ \frac{\begin{array}{l} {t_1}:{B_{272}}, {t_2}:{B_1}, {t_3}:{B_{273}}, {t_4}:{B_{274}}, {t_5}:{B_{275}}, {t_6}:{B_{276}}, {t_7}:{B_{277}}, {t_8}:{B_{278}}, {t_9}:{B_{279}}, {t_{10}}:{B_{280}}, \\ t = ({t_1}, {t_2}, {t_3}, {t_4}, {t_5}, {t_6}, {t_7}, {t_8}, {t_9}, {t_{10}}), \\ {T_{14}} = {B_{272}} \times {B_1} \times {B_{273}} \times {B_{274}} \times {B_{275}} \times {B_{276}} \times {B_{277}} \times {B_{278}} \times {B_{279}} \times {B_{280}} \end{array}}{{t:{T_{14}}}}({\rm{TR4}}) $

即, 输入项t所属的类型为T₁₄.