R-演算:一个修正程序规约的演算系统
| 文献类型 | 期刊 |
| 作者 | 李未[1] |
| 机构 | [1]北京航空航天大学软件开发环境国家重点实验室 北京100083 ↓ |
| 来源信息 | 年:2002卷:32期:5页码范围:662-673 |
| 期刊信息 | 中国科学E辑ISSN:1006-9275 |
| 关键词 | 软件规约;事实反驳;必要前提;修正演算 |
| 摘要 | 在一个软件规约(program specification)的形成过程中,规约总是不断被修改,要么增加新的功能,要么由于出现事实反驳,而改正规约中的错误.规约的新功能是与其逻辑无关的新规则,而它的事实反驳则是其反例.新规则和事实反驳都是由研究者或用户提出来的.极大缩减是在规约出现事实反驳的情况下,对规约的理想修正.这里在一阶逻辑的框架下给出规约的新规则、事实反驳和极大缩减的模型论定义.构建了R-演算.该演算由一组变换规则组成,用以删除规约中与事实反驳矛盾的规则,并最终得到规约的极大缩减.同时证明了R-演算的可达性和完全性. |
| 所属部门 | 计算机学院；校机关 |
| 链接地址 | http://d.g.wanfangdata.com.cn/Periodical_zgkx-ce200205012.aspx |
| DOI | 10.3321/j.issn:1006-9275.2002.05.012 |
| 人气指数 | 2 |
| 浏览次数 | 2 |
| 基金 | 科技部科研项目; 中国科学院资助项目 |
全文
影响因子：
计算机学院
dc:title:R-演算:一个修正程序规约的演算系统
dc:creator:李未
dc:date: publishDate:2002-10-20
dc:type:期刊
dc:format: Media：中国科学E辑
dc:identifier: LnterrelatedLiterature：中国科学E辑.2002,32(5),662-673.
dc:identifier:DOI：10.3321/j.issn:1006-9275.2002.05.012
dc: identifier:ISBN:1006-9275
