基于类型理论的领域数据建模和验证及案例

摘要

数据作为软件系统的主要处理对象,其规范性有助于软件系统的设计开发和软件系统之间的数据交换.面向行业数据规范及其验证,提出了一种基于类型理论的领域数据建模语言(DDML)和领域建模方法(DDMM).DDML语言通过定义类型和项的语法和语义,描述领域数据类型和对象的结构,通过定义类型规则及其类型检查算法判定任意项t:T?.DDMM给出了领域数据建模的方法,即构建K1(原子类型)、K2(数据元)、κ3(数据元目录)三层框架,生成表示K3层数据元目录之间关系的类型规则.在此基础上,给出了数据元目录序列的定义及其正确性判定算法.基于上述方法,实现了一种领域数据建模工具原型系统,并通过领域数据建模与自动验证的一个实际案例,完成了一个较大规模行业数据规范的制定与验证.%As the main object manipulated by a software system,data with a domain standard can contribute to the process of software design and data shareware between software systems.In this paper,focusing on domain data standardization,a domain data modelling language (DDML) and a domain data modelling method (DDMM based on the type theory are proposed.In DDML,the syntax and semantics of types and terms are defimed to describe the structure of the domain data types and objects,and the typing rules are defined to process the judgement of t:T.For DDMM,the data modelling processes are presented with the data modelling of K1 (atomic type),K2 (data element),κ3 (data element directory) and the generation of typing rules in K3.Furthermore,the definition of the data element directory sequences and the algorithms of checking its correctness are defined.Finally,a prototype of the domain data modelling system as a modelling tool is developed and applied to a real case of large scale by the generation of the domain data standard and its evaluation.