R-演算:一个修正程序规约的演算系统  

作　　者：李未[1] 

机构地区：[1]北京航空航天大学软件开发环境国家重点实验室,北京100083

出　　处：《中国科学（E辑）》2002年第5期662-673,共12页Science in China(Series E)

基　　金：国家"九七三"海量信息重大基础研究项目(G1999032701);国家自然科学基金资助项目(批准号:90104008)

摘　　要：在一个软件规约（Program specification）的形成过程中,规约总是不断被修改,要么增加新的功能,要么由于出现事实反驳,而改正规约中的错误.规约的新功能是与其逻辑无关的新规则,而它的事实反驳则是其反例.新规则和事实反驳都是由研究者或用户提出来的.极大缩减是在规约出现事实反驳的情况下,对规约的理想修正.这里在一阶逻辑的框架下给出规约的新规则、事实反驳和极大缩减的模型论定义.构建了R-演算.该演算由一组变换规则组成,用以删除规约中与事实反驳矛盾的规则,并最终得到规约的极大缩减.同时证明了R-演算的可达性和完全性.

关 键 词：软件规约 事实反驳 必要前提 修正演算 R—演算 程序规约 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]