内含定理证明器的程序开发系统

孙永强; 杨继锋; 陆朝俊; 邵志清

首页> 中文期刊> 《上海交通大学学报》 >内含定理证明器的程序开发系统

内含定理证明器的程序开发系统

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

提出了一个基于重写技术的程序开发系统，它提供了扩展的函数式语言和代数规约语言相结合的混合语言，该语言中引入了优化规则和测试等式说明机制．优化规则用于优化代码和满足某些特殊需求．运用测试等式说明机制可使程序员在程序中给出一些用于测试的等式，对程序进行测试，这些测试是在被开发系统形成前进行的．对优化规则和测试等式的证明，是由系统中的证明子系统（定理证明器）完成的．定理证明器的引入，提高了所开发系统的正确性，并且有利于缩短系统的开发周期．

著录项

来源
《上海交通大学学报》 |1998年第10期|42-45|共4页
作者
孙永强; 杨继锋; 陆朝俊; 邵志清;
展开▼
作者单位

上海交通大学计算机科学与工程系;

华东理工大学计算机科学系;

展开▼
原文格式 PDF
正文语种 chi
中图分类软件工程;
关键词
函数式语言; 软件工程; 程序开发系统; 定理证明器;

相似文献

中文文献
外文文献
专利

1. 运用定理证明器ACL2验证机器人操作系统ROS节点间通信 [J] . 高雅 ,李晓娟 ,关永 . 小型微型计算机系统 . 2014,第009期
2. 定理证明器 Coq 与机械语义研究 [J] . 窦亮 ,刘强 ,杨宗源 . 计算机应用与软件 . 2015,第010期
3. 语义Tableau定理证明器的Prolog实现 [J] . 高华 ,江建国 ,苏贺靓 . 科技视界 . 2015,第009期
4. 一个用于指针程序验证的自动定理证明器的设计与实现 [J] . 王振明 ,陈意云 ,王志芳 . 小型微型计算机系统 . 2010,第005期
5. COQ定理证明器辅助PLC程序验证和分析 [J] . 陈钢 ,宋晓宇 ,顾明 . 北京大学学报：自然科学版 . 2010,第1期
6. 使用定理证明器ANDP简化构造几何公理系统 [C] . 李大法 . 第五届中国人工智能联合学术会议 . 1998
7. 图论在定理证明器HOL4中的形式化 [A] . 安亚鹏 . 2021

内含定理证明器的程序开发系统

摘要

著录项

相似文献

相关主题

期刊订阅