软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2000年
8期
1066-1070
,共5页
函数程序设计语言%代数规范%项重写系统%定理 证明%无归纳的归纳法
函數程序設計語言%代數規範%項重寫繫統%定理 證明%無歸納的歸納法
함수정서설계어언%대수규범%항중사계통%정리 증명%무귀납적귀납법
完整地介绍了一个基于重写技术的程序开发和验证系统,重点展示验证子系统的理论、方法和技术.验证子系统使得系统能自动证明程序和规范中的优化规则及测试等式,从而进一步保证程序开发过程的正确性.验证子系统所采用的主要技术是以成批证明方法和证据测试集为特色的重写归纳方法.
完整地介紹瞭一箇基于重寫技術的程序開髮和驗證繫統,重點展示驗證子繫統的理論、方法和技術.驗證子繫統使得繫統能自動證明程序和規範中的優化規則及測試等式,從而進一步保證程序開髮過程的正確性.驗證子繫統所採用的主要技術是以成批證明方法和證據測試集為特色的重寫歸納方法.
완정지개소료일개기우중사기술적정서개발화험증계통,중점전시험증자계통적이론、방법화기술.험증자계통사득계통능자동증명정서화규범중적우화규칙급측시등식,종이진일보보증정서개발과정적정학성.험증자계통소채용적주요기술시이성비증명방법화증거측시집위특색적중사귀납방법.
