| R-演算:一个修正程序规约的演算系统 |
| |
| 作者姓名： | 李未 |
| |
| 作者单位： | 北京航空航天大学软件开发环境国家重点实验室,北京,100083 |
| |
| 基金项目： | 国家“九七三”海量信息重大基础研究项目（G1999032701），国家自然科学基金资助项目（批准号:90104008） |
| |
| 摘 要： | 在一个软件规约(program specification)的形成过程中, 规约总是不断被修改, 要么增加新的功能, 要么由于出现事实反驳, 而改正规约中的错误. 规约的新功能是与其逻辑无关的新规则, 而它的事实反驳则是其反例. 新规则和事实反驳都是由研究者或用户提出来的. 极大缩减是在规约出现事实反驳的情况下, 对规约的理想修正. 这里在一阶逻辑的框架下给出规约的新规则、事实反驳和极大缩减的模型论定义. 构建了R-演算. 该演算由一组变换规则组成, 用以删除规约中与事实反驳矛盾的规则, 并最终得到规约的极大缩减. 同时证明了R-演算的可达性和完全性.
|
| 关 键 词： | 事实反驳 必要前提 修正演算 软件规约 |
| 收稿时间： | 2002-04-15 |
| 修稿时间： | 2002-08-16 |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《中国科学(E辑)》浏览原始摘要信息 |
|
点击此处可从《中国科学(E辑)》下载全文 |
|
