结构化面向对象形式规格说明语言OOZS——类型检查器 被引量：1

1

作者 李刚 朱关铭 缪淮扣 《上海大学学报（自然科学版）》 CAS CSCD 1998年第5期572-578,共7页

ＯＯＺＳ类型检查器是ＯＯＺＳ规格说明的一种检查程序，它可以找出用户编写的ＯＯＺＳ规格说明中出现的语法错误以及类型操作的不一致错误，并能够自动定位错误．本文介绍了ＯＯＺＳ类型检查器的设计与实现．

关键词 语法分析 YACC OOZS 类型检查器 软件工程

下载PDF 职称材料

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

2

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

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

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

下载PDF 职称材料

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

3

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

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

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

下载PDF 职称材料

强附类型和动态类型检查

4

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

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

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

下载PDF 职称材料

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

5

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

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

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

下载PDF 职称材料

附类型Smalltalk及其类型检查

6

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

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

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

下载PDF 职称材料

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

7

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

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

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

下载PDF 职称材料

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

8

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

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

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

下载PDF 职称材料

医用X射线CT主要检查类型所致成年受检者剂量的探讨 被引量：2

9

作者 刘艳玲 孙希同 《中国医药指南》 2018年第14期296-297,共2页

本文主要研究了医用X射线CT主要检查类型所致成年受检者剂量,调查了X-CT机不同品牌和在医院中所使用的比例情况。总共针对8种常见主要检查类型的112例成年受检者,研究了这些成年受检者在进行X-CT检查时,所使用的扫描参数和相关剂量学信... 本文主要研究了医用X射线CT主要检查类型所致成年受检者剂量,调查了X-CT机不同品牌和在医院中所使用的比例情况。总共针对8种常见主要检查类型的112例成年受检者,研究了这些成年受检者在进行X-CT检查时,所使用的扫描参数和相关剂量学信息,并通过剂量转换来计算所致典型的有效剂量。通过研究表明,需要对X-CT扫描检查的影像质量进行加强,并需要对所致剂量进行优化匹配的研究,特别需要注意的是要选取合适的各类X-CT检查所使用的扫描参数,同时还需要完善X-CT检查的医疗照射指导水平。 展开更多

关键词 医用X射线 CT主要检查类型 成年受检者剂量

下载PDF 职称材料

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

10

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

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

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

下载PDF 职称材料

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

11

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

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

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

下载PDF 职称材料

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

12

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

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

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

下载PDF 职称材料

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

13

作者 乌尼日其其格 李小平 +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 职称材料

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

14

作者 乌尼日其其格 李小平 +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

15

作者 李小平 乌尼日其其格 +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 职称材料

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

16

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

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

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

下载PDF 职称材料

一个定理证明检查器

17

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

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

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

下载PDF 职称材料

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

18

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

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

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

下载PDF 职称材料

急诊内科急性腹痛的治疗方法及其疗效评估

19

作者 彭子俊 李国涛 +2 位作者 加尔肯·拉斯拜 冯颖 侯秀丽 《中文科技期刊数据库（引文版）医药卫生》 2024年第8期0109-0112,共4页

通过对急性腹痛的病因分类以及症状的发展情况进行统计,并进一步探讨其治疗方法效果的评估。方法 选取收治的120例急性腹痛患者为研究对象,将其按照病因分为急性胃炎、急性肠胃炎、消化性胃溃疡、急性阑尾炎及急性胆囊炎等5组。所有患... 通过对急性腹痛的病因分类以及症状的发展情况进行统计,并进一步探讨其治疗方法效果的评估。方法 选取收治的120例急性腹痛患者为研究对象,将其按照病因分为急性胃炎、急性肠胃炎、消化性胃溃疡、急性阑尾炎及急性胆囊炎等5组。所有患者均进行适当的治疗,并对治疗后的症状缓解情况进行评估。同时,对患者的检查类型及检查结果进行统计,以确认确诊的比例。结果 急性胃炎(28.33%)、急性肠胃炎(25%)、消化性胃溃疡(20.83%)、急性阑尾炎(15.83%)及急性胆囊炎(10%)为急性腹痛的主要病因。不同病因的症状缓解有效率均达到了89.47%以上。其中,通过血常规、腹部CT、腹部X线、腹部B超、胃镜等检查,确诊率分别为80.87%,82.57%,82.43%,83.33%,86.96%。结论 对于急诊内科的急性腹痛,各种治疗方法的疗效显著,症状缓解情况良好,但要针对具体病因选择合适的治疗方法。并结合各种检查手段来提高准确的确诊率,尽早为患者进行效果良好的治疗。 展开更多

关键词 急性腹痛 疗效评估 病因分类 检查类型 治疗方法

下载PDF 职称材料

隔爆型电气设备的检查

20

作者 张玉大 王方利 《电气防爆》 2013年第3期26-29,共4页

简要介绍了隔爆型电气设备的基本检查要求、检查等级、类型、项目要求。

关键词 隔爆型 检查类型 检查等级 检查要求

下载PDF 职称材料