形式化方法B的证明技术 被引量：4

1

作者 鹿蕾 《现代电子技术》 2005年第23期126-128,共3页

用形式化方法开发软件是提高软件可靠性和开发效率并实现其自动化的关键。形式化方法B是借助于其辅助工具支持从规约到实现的全过程开发工作。本文介绍了B方法的分层开发与证明过程,针对构造AM以及对他进行精化和实现过程中的类型检查... 用形式化方法开发软件是提高软件可靠性和开发效率并实现其自动化的关键。形式化方法B是借助于其辅助工具支持从规约到实现的全过程开发工作。本文介绍了B方法的分层开发与证明过程,针对构造AM以及对他进行精化和实现过程中的类型检查、证明义务进行了重点分析,最后通过具体应用说明了B方法的证明技术在实践中的有效性。 展开更多

关键词 形式化方法 抽象机 广义代换 类型检查 证明义务

下载PDF 职称材料

基于类型理论的领域数据建模和验证及案例 被引量：4

2

作者 乌尼日其其格 李小平 +1 位作者 马世龙 吕江花 《软件学报》 EI CSCD 北大核心 2018年第6期1647-1669,共23页

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

关键词 类型理论 类型检查 类型规则 领域数据建模 数据规范

下载PDF 职称材料

用Xerces-J进行基于XML Schema的XML局部验证 被引量：2

3

作者 张昱 李凡 《小型微型计算机系统》 CSCD 北大核心 2005年第8期1369-1373,共5页

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

关键词 XML SCHEMA 局部验证 类型检查 ID约束检查

下载PDF 职称材料

一种带约束的多态类型系统 被引量：3

4

作者 郑红军 张乃孝 《计算机学报》 EI CSCD 北大核心 1999年第4期343-350,共8页

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

关键词 约束类型 类型检查 多态类型系统 程序设计语言

下载PDF 职称材料

高阶类型化软件体系结构建模和验证及案例 被引量：2

5

作者 乌尼日其其格 李小平 +2 位作者 马世龙 吕江花 张思卿 《软件学报》 EI CSCD 北大核心 2019年第7期1916-1938,共23页

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

关键词 类型规则 类型检查 软件体系结构 软件体系结构建模 软件体系结构验证

下载PDF 职称材料

基于分层思想的变量类型提取方法 被引量：1

6

作者 甘玲 汤睿 《重庆邮电学院学报（自然科学版）》 2006年第4期539-543,共5页

提出了一种基于分层思想的,并且无需构造具体语法树的变量类型提取方法。目的是为高级语言的类型信息的提取提供一般方法,从而降低类型系统实现的难度以及产生程序错误的可能性,并且简化高级语言的中间表示,便于后端的代码生成和优化。

关键词 编译器 类型树 类型提取 类型检查 类型系统

下载PDF 职称材料

一类递归函数的多态类型 被引量：1

7

作者 黄文集 《软件学报》 EI CSCD 北大核心 2004年第7期969-976,共8页

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

关键词 函数式语言 多态 类型检查 递归函数 类型系统

下载PDF 职称材料

高阶类型化可验证应用系统体系结构建模及案例 被引量：1

8

作者 李小平 乌尼日其其格 +1 位作者 马世龙 吕江花 《软件学报》 EI CSCD 北大核心 2020年第8期2309-2335,共27页

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

关键词 类型规则 类型检查 部署方案 应用系统体系结构建模 应用系统体系结构验证

下载PDF 职称材料

规格说明语言Z的类型检查 被引量：1

9

作者 张晓莺 朱关铭 缪淮扣 《计算机应用与软件》 CSCD 2000年第2期1-9,29,共10页

软件规格说明的正确性是软件目标代码正确性的前提。正确性要求之一就是类型正确。本文介绍Z规格说明类型检查器的实现方法,并对类型检查的环境、一致化方法、替换策略和类型变量的应用等问题进行讨论。

关键词 类型检查 规格说明语言 Z语言 形式谱义

下载PDF 职称材料

基于SOFL规范的语义分析 被引量：1

10

作者 高正华 陈昊鹏 《计算机应用与软件》 CSCD 北大核心 2007年第11期86-88,共3页

传统的形式化方法局限于严格的证明、对程序员要求较高的教育背景,使其举步维艰。于是作为形式化方法与面向对象的联姻的SOFL(Structured Object-Oriented Formal Language)便应运而生。在给出语义分析的整体算法后,逐步分析各个阶段遇... 传统的形式化方法局限于严格的证明、对程序员要求较高的教育背景,使其举步维艰。于是作为形式化方法与面向对象的联姻的SOFL(Structured Object-Oriented Formal Language)便应运而生。在给出语义分析的整体算法后,逐步分析各个阶段遇到的关键问题并给出解决方法,同时在参考其他语言的基础上,定义了SOFL中一些语义规则。 展开更多

关键词 抽象生成树(AST) 访问者模式 符号表 作用域 SOFL 类型检查

下载PDF 职称材料

参数化类型及动态类型检查

11

作者 梅宏 孙永强 《应用科学学报》 CAS CSCD 1994年第4期325-332,共8页

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

关键词 程序语言 数据类型 参数化类型 类型检查

下载PDF 职称材料

采用了剪枝优化的子类型关系判定算法

12

作者 戴晓君 陈海明 《软件学报》 EI CSCD 北大核心 2010年第7期1481-1490,共10页

静态类型化XML处理语言为处理XML数据提供了新的途径,但现有的此类语言大多数效率较低.研究此类语言的一个重要问题——子类型关系的判定,并使用剪枝优化策略对XDuce的子类型关系判定算法进行优化.实验数据显示,优化后算法的执行效率平... 静态类型化XML处理语言为处理XML数据提供了新的途径,但现有的此类语言大多数效率较低.研究此类语言的一个重要问题——子类型关系的判定,并使用剪枝优化策略对XDuce的子类型关系判定算法进行优化.实验数据显示,优化后算法的执行效率平均提高20%.该策略具有普遍性,对所有使用类似算法的静态类型化XML处理语言都有效. 展开更多

关键词 XML 静态类型化语言 类型检查 子类型关系判定 算法优化

下载PDF 职称材料

一个定理证明检查器

13

作者 顾永立 顾训穰 谢步罡 《上海大学学报（自然科学版）》 CAS CSCD 2000年第1期63-66,共4页

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

关键词 类型检查 定理证明 归约 重命名 演算 检查器

下载PDF 职称材料

一个经过证明的类型化汇编语言的类型检查器

14

作者 郭宇 陈意云 +1 位作者 华保健 李兆鹏 《小型微型计算机系统》 CSCD 北大核心 2008年第7期1230-1236,共7页

编程语言类型系统的类型安全性可以保证程序运行时满足基本安全属性,包括控制流安全,内存安全等.类型化编程语言都需要一个类型检查器来检查程序的良类型性,因此编程语言的具体实现是否能保证类型安全性,还依赖类型检查器的可靠性.本文... 编程语言类型系统的类型安全性可以保证程序运行时满足基本安全属性,包括控制流安全,内存安全等.类型化编程语言都需要一个类型检查器来检查程序的良类型性,因此编程语言的具体实现是否能保证类型安全性,还依赖类型检查器的可靠性.本文给出一种类型化汇编语言,然后给出相应的类型检查器,并证明了此类型检查器的可靠性,从而保证经过类型检查的汇编程序的安全性.文本的所有工作,包括类型化汇编语言、类型检查器以及相关定理证明,均已在证明辅助工具Coq中实现.本文方法也可用于证明类型化高级语言的类型检查器的可靠性. 展开更多

关键词 类型系统 汇编语言 类型检查 软件安全

下载PDF 职称材料

附类型Smalltalk及其类型检查

15

作者 梅宏 《微电子学与计算机》 CSCD 北大核心 1993年第2期23-26,共4页

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

关键词 程序设计 程序语言 类型检查 类型

下载PDF 职称材料

强附类型和动态类型检查

16

作者 梅宏 孙永强 《小型微型计算机系统》 CSCD 北大核心 1992年第10期23-28,34,共7页

数据类型是程序语言中的一个重要概念,编译时类型检查(静态检查)和运行时类型检查(动态检查)是两种主要的类型检查方式,各自有着自己的优点。本文提出一种类型检查模式,即强附类型—动态检查,作为这两种方式的折衷,并讨论了其在语言中... 数据类型是程序语言中的一个重要概念,编译时类型检查(静态检查)和运行时类型检查(动态检查)是两种主要的类型检查方式,各自有着自己的优点。本文提出一种类型检查模式,即强附类型—动态检查,作为这两种方式的折衷,并讨论了其在语言中的应用和优点。 展开更多

关键词 程序语言 数据类型 类型检查

下载PDF 职称材料

基于类型化内存地址的安全策略的设计与实现

17

作者 郭帆 陈意云 胡荣贵 《计算机研究与发展》 EI CSCD 北大核心 2003年第7期1001-1007,共7页

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

关键词 类型安全策略 证明方法 类型检查 代码安全 逻辑表示 形式化描述

下载PDF 职称材料

可组合的描述符泄露类型检查

18

作者 李沁 缪瑨 《计算机科学》 CSCD 北大核心 2015年第10期184-188,共5页

应用程序通过操作系统的系统调用对文件描述符进行操作并管理文件资源。如果应用程序对资源描述符的管理出现错误并发生描述符泄漏,会严重影响系统的可用性。据此,提出了一种检查程序是否会导致描述符泄漏的类型系统,给出了描述符操作... 应用程序通过操作系统的系统调用对文件描述符进行操作并管理文件资源。如果应用程序对资源描述符的管理出现错误并发生描述符泄漏,会严重影响系统的可用性。据此,提出了一种检查程序是否会导致描述符泄漏的类型系统,给出了描述符操作方法的语义和类型约束,证明了类型系统的可靠性定理。此外,还初步讨论了该类型系统在并发程序下的扩展。 展开更多

关键词 描述符泄露 类型检查 软件安全

下载PDF 职称材料

正规树文法的产生式相交判定 被引量：2

19

作者 倪晓勇 陈海明 《计算机工程与设计》 CSCD 北大核心 2012年第3期1197-1202,1212,共7页

在针对产生式不相交的正规树文法的XML类型检查中,需要对正规树文法的产生式进行相交判定。基于正规树文法的产生式的构成特点,提出了基于自动机的相交判定算法。根据产生式的内容模型即正则表达式,构建相应自动机,判定两个自动机的交... 在针对产生式不相交的正规树文法的XML类型检查中,需要对正规树文法的产生式进行相交判定。基于正规树文法的产生式的构成特点,提出了基于自动机的相交判定算法。根据产生式的内容模型即正则表达式,构建相应自动机,判定两个自动机的交是否为空,该算法的时间复杂度为O(‖E1‖.‖E2‖.|∑E1∪∑E2|)。实验结果表明,该算法运行正确且高效,可以应用到针对产生式不相交的正规树文法的XML类型检查中。 展开更多

关键词 XML类型检查 正规树文法 产生式 相交判定 正则表达式 自动机

下载PDF 职称材料

面向对象语言自然类型检查方法

20

作者 王丹 王斌 杨元生 《大连理工大学学报》 CAS CSCD 北大核心 2001年第2期249-252,共4页

针对面向对象技术中由于多态等机制导致的类型不安全问题 ,提出一种解决方案——自然类型检查 .该方法对面向对象程序设计中的变量进行类型安全检查 ,发现由多态、强制类型转换等机制引入的不安全因素 ,保证程序的正确执行 .以 Java为... 针对面向对象技术中由于多态等机制导致的类型不安全问题 ,提出一种解决方案——自然类型检查 .该方法对面向对象程序设计中的变量进行类型安全检查 ,发现由多态、强制类型转换等机制引入的不安全因素 ,保证程序的正确执行 .以 Java为描述语言 ,详细介绍了该方法 ,并与传统的类型检查进行了比较 . 展开更多

关键词 面向对象 多态 类型安全检查 程序设计方法 自然类型检查 类型不安全问题 JAVA

下载PDF 职称材料