-
题名面向对象程序设计语言的形式语义研究
被引量:2
- 1
-
-
作者
瞿裕忠
王志坚
徐家福
-
机构
南京大学计算机软件研究所
-
出处
《计算机科学》
CSCD
北大核心
1995年第2期6-10,共5页
-
文摘
面向对象程序设计语言(以下简称面向对象语言)的基本思想起源于六十年代中期的Simula语言,在七十年代的Smalltalk语言及环境中得到发展,在八十年代的Eiffel、C++等语言中进一步得到巩固和完善。
-
关键词
程序语言
面向对象
形式语义
程序设计
-
Keywords
programming languge,object-oriented programming language,formal semantic.
-
分类号
TP312
[自动化与计算机技术—计算机软件与理论]
TP301.2
[自动化与计算机技术—计算机系统结构]
-
-
题名程序设计语言的形式语义研究进展
被引量:3
- 2
-
-
作者
计春雷
-
机构
上海电机学院电子信息学院
-
出处
《上海电机学院学报》
2007年第3期204-209,共6页
-
文摘
程序设计语言形式语义描述方法的产生与发展,对程序设计语言的设计和标准化,编译程序的设计和优化,程序推理,以及协议形式化描述、分析验证与设计等都有着重要的意义。回顾形式语义描述方法的研究发展史,介绍当前主要的语义形式描述方法,并给出这些方法的评价标准和比较结果;指出最有发展潜力的语义描述方法以及将来的发展方向。
-
关键词
形式语义
程序设计语言
描述方法
发展
-
Keywords
formal semantics
programming languages
description techniques
progress
-
分类号
TP317
[自动化与计算机技术—计算机软件与理论]
-
-
题名一个说明语言的设计和其子集编译器的开发
- 3
-
-
作者
江国华
张庆明
-
机构
南京航空航天大学计算机科学与工程系
云南软件技术开发中心
-
出处
《南京航空航天大学学报》
CAS
CSCD
1996年第3期419-426,共8页
-
文摘
基于软件文档可执行的想法,设计了一个适用于指称语义描述的可执行规范说明语言——JZC,并对其核心子集编译器进行了设计与开发。该语言设计采用了模式匹配、类型并置和构造函数等概念,使得抽象文法易于在程度中体现。模块概念的引入使得函数型语言书写的程序更加易懂和易于编写。作为对严格开发方法的一个尝试,JZC核心子集编译器的开发采用了该种方法,其中一个“结果正确性定理”的证明是开发过程的重点工作。本文通过一个示例语言简介JZC的语言特点。
-
关键词
编译程序
程序语言
形式语言
指称语义
-
Keywords
compiler
programming language
formal language
rigorous approach
denotation semantics
-
分类号
TP314
[自动化与计算机技术—计算机软件与理论]
-
-
题名一种面向对象的函数式语言
- 4
-
-
作者
赵东范
李微
张扬
-
机构
长春邮电学院计算机工程系
吉林省电力局
-
出处
《长春邮电学院学报》
1999年第1期18-25,共8页
-
文摘
设计了一种对象式和函数式相结合的混合型语言OOFL(面向对象的函数式语言),详细给出了它的语法及语义定义,提出了相应的实现方案,并在微机上实现了OOFL到C++的转换系统。从而提供了一种面向对象机制的描述工具。
-
关键词
程序语言
形式语言
程序文法
程序变换
-
Keywords
program language
formal language
program grammar
program transfarming
Object
semantic
semantic domain
-
分类号
TP312
[自动化与计算机技术—计算机软件与理论]
-
-
题名一个C语言子集上的程序逻辑
被引量:1
- 5
-
-
作者
王勇朝
李兆鹏
冯新宇
-
机构
中国科学技术大学计算机科学与技术学院
中国科学科技大学苏州研究院软件安全实验室
-
出处
《小型微型计算机系统》
CSCD
北大核心
2014年第6期1258-1264,共7页
-
基金
国家自然科学基金项目(61073040
61170018
61003043)资助
-
文摘
在分离逻辑和C语言规范的基础上,设计一个C语言子集C3(C Code Certified)上的程序逻辑,其由操作语义、推导规则和可靠性证明组成.操作语义采用了小步的方式,为并发程序的验证留下了扩展的可能性.推导规则采用了扩展Hoare三元组的形式,易于程序员的理解,支持了更多的C语言特征.证明可靠性需要在语义上定义推导规则,本文采用了广为接受的直接定义方式,本文可靠性的证明在Coq中实现,并提供了一份可以通过机器自动检查的证明,保证了逻辑的可信度.证明实例展示了程序逻辑的可用性,程序验证工具可以直接使用C3的推导规则,简化验证的过程.
-
关键词
C语言
小步语义
程序逻辑
可靠性
形式化验证
-
Keywords
C language
small-step semantics
program logic
soundness
formal verification
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名步进索引模型下的语义及其形式化
- 6
-
-
作者
郭昊
曹钦翔
-
机构
上海交通大学电子信息与电气工程学院
-
出处
《软件学报》
EI
CSCD
北大核心
2022年第6期2127-2149,共23页
-
基金
国家自然科学基金青年科学基金(61902240)。
-
文摘
霍尔逻辑作为计算机程序的逻辑基础,可以用于描述一般程序的验证.分离逻辑作为霍尔逻辑的扩展,可以支持很多现代程序语言中的高阶特性.步进索引模型被用于定义自递归谓词.步进索引逻辑被广泛应用于各种基于交互式定理证明器的程序验证工具中,然而,基于步进索引逻辑的推理却比经典逻辑复杂、繁琐.事实上,也可以在步进索引模型上定义更加简洁清晰的、与“步数”无关的经典逻辑体系下的非步进索引程序语义.人们希望找到步进索引逻辑和非步进索引逻辑之间的关系,但发现两种逻辑并不等价.对实际的程序验证工作中涉及的命题进行归纳总结,找出它们共同的特征,给出关于程序状态的断言的约束条件;分别定义步进索引逻辑和非步进索引逻辑体系中断言的语义,并证明在该约束条件下两种语义的等价性;在Coq中,形式化以上所有定义和证明;最后,对未来值得关注的研究方向进行初步探讨.
-
关键词
程序状态模型
程序语言的语义
形式化验证
-
Keywords
model of program states
semantics of programming language
formal verification
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-