摘要：数据类型是程序设计语言设计中的一个重要概念。该文通过对Ｍｉｌｎｅｒ多态类型系统的扩展，提出了一个允许将类型作为一阶对象处理的参数化类型系统，并给出了相应的动态类型检查规则。

摘要：Smalltalk的有效实现是一个有趣的研究课题。类型系统是编译代码优化的前提。本文讨论了一个Smalltalk类型系统及其类型检查方式:静态附类型——动态检查。这个类型系统不仅提供了编译优化信息,还保持了动态联编带来的系统灵活性。

摘要：根据权威统计数据,软件测试中发现的70%以上的错误由需求获取或体系结构设计引起.因此,应用软件体系结构在设计阶段的正确性验证非常重要.现有的软件体系结构设计方法不支持需求满足验证,需求满足验证需要其他验证工具的支持.面向主流Web应用软件的体系结构设计及其需求满足验证,提出了一种高阶类型化软件体系结构建模和验证语言(SAML)与软件体系结构建模和验证方法(SAMM).SAML语言通过定义类型和项的语法及语义,描述软件体系结构中类型和对象的构造,通过定义类型规则及其类型检查算法来判定Γ┝t:T和Γ┝R(T1, T2)是否成立.SAMM给出了软件体系结构建模范式,包括构建接口类型Mcls(typeinterface)、组件Mcmpt(component)、容器Mcont(container)、框Mfrm(frame)和框架Mfrwk(framework)这5层建模过程,以及生成层内与层间类型之间关系对应的类型规则,同时定义了接口类型方法调用图(GSA)用以刻画软件体系结构设计要求,定义了类型序列及其正确性用以刻画需求期望的性质,并给出了相应的验证算法.设计实现了基于该方法的原型工具系统SAMVS,其中,模型编辑环境支持应用软件的设计过程,验证环境支持设计满足需求的自动化验证.通过一个实际案例,完成了一个较大规模"互联网+"应用软件系统的体系结构建模和验证.

摘要：随着应用软件体系结构风格变化和规模变大,其运行环境变得日趋复杂,对应用系统体系结构的设计及其正确性验证提出了新的挑战.现有的应用系统体系结构设计关于需求满足性验证在建模与验证中需要多种工具的支持.应用系统体系结构在设计阶段的需求满足验证,有助于客观评价应用系统部署方案和系统如期上线以及主动运维.面向应用系统体系结构设计及其验证,在模型驱动的软件工程背景下提出一种高阶类型化可验证应用系统体系结构建模语言(VASAML)与可验证应用系统体系结构建模方法(VASAMM).VASAML语言通过定义类型和项的语法和语义,描述构成应用系统体系结构的类型和对象的结构,通过定义两种类型规则及其类型检查算法,判定Γt:T和ΓR(T1,T2)是否成立,其中,结构类类型规则用于描述应用系统体系结构中的组成部分,关系类类型规则用于描述组成部分之间的关系和配置.VASAMM方法给出了应用系统体系结构建模过程,包括构建Mbd(基本数据类型)、Mbti(基本接口类型)、Mdev(设备类型)和Mfrwk(应用系统框架)这4层,以及自动生成层内与层间类型之间关系对应的类型规则,同时定义了设备类型服务调用图(GDSI)用以刻画部署要求,定义了类型序列及其正确性用以刻画需求期望性质,并给出了相应的基于类型检查的验证算法.设计实现了基于该方法的原型工具系统VASAMS,其中,建模编辑环境支持应用系统部署方案的设计过程,验证环境支持设计是否满足需求的自动验证.通过一个实际案例完成了某行业较大规模应用系统体系结构的建模和验证.

摘要：提出了一种检查代码安全的类型安全策略 ,详细描述了该策略的逻辑表示、形式化描述和基于该策略的证明方法 ,最后给出一个基于该策略的定理证明器HBTSTP 策略的核心思想是给每个合法的内存地址赋予类型 ,使用符号表达式记录内存的状态变化 ,对于需要读写内存的指令 ,调用证明器进行类型检查 。

摘要：本文讨论了一种带约束的多态类型系统，引入了约束类型．约束与全称量化的结合使得参数化多态函数的应用更安全，同时也为重载的表示和实现提供了一个新的途径，提高了类型表示的抽象度本文讨论的类型系统具有两个不同层次的类型结构，约束的引入与消去是不同层次上的操作．最后，本文绘出了类型检查算法Wτ，并证明了此算法中约束的可满足性是可判定的．

摘要：以上下文无关语言上的递归函数为基础的语言LFC(languageforcontextfreerecursivefunction)是一种形式规约语言,适于处理短语结构.LFC也是函数式语言,具有函数式语言的许多特点.LFC已经在形式规约获取系统SAQ(specificationacquisitionsystem)中实现,为其最初设计的类型系统不支持多态类型.引入类型变量和相应的类型检查方法,就可以将其类型系统扩充为多态类型系统.对多态类型系统实现中的一些问题也进行了讨论.在实现多态之后,LFC的灵活性将得到增强,从而会为其应用创造更为有利的条件.

摘要：数据作为软件系统的主要处理对象,其规范性有助于软件系统的设计开发和软件系统之间的数据交换.面向行业数据规范及其验证,提出了一种基于类型理论的领域数据建模语言(DDML)和领域建模方法(DDMM).DDML语言通过定义类型和项的语法和语义,描述领域数据类型和对象的结构,通过定义类型规则及其类型检查算法判定任意项t:T?.DDMM给出了领域数据建模的方法,即构建K_1(原子类型)、K_2(数据元)、K_3(数据元目录)三层框架,生成表示K_3层数据元目录之间关系的类型规则.在此基础上,给出了数据元目录序列的定义及其正确性判定算法.基于上述方法,实现了一种领域数据建模工具原型系统,并通过领域数据建模与自动验证的一个实际案例,完成了一个较大规模行业数据规范的制定与验证.

摘要：XML验证,特别是局部验证,是XML应用中的一个关键问题.调研分析了Xerces-J2工具包中的基于XMLSchema的XML解析、验证体系,它是一种延迟的整体验证.利用Xerces-J2,设计实现了基于XMLSchema的XML局部验证接口,包括类型检查和ID约束检查等.

摘要：介绍了一种新型的形式说明语言 PD_ Cal,该语言具有良好的表达能力以及丰富的类型 .通过对由该语言描述的定理证明过程进行类型检查 ,可判断该证明是否是给定定理的正确的证明 .在该思想的基础上 ,设计并实现了PD_ Cal定理证明检查器 .