互逆主义程序精化——程序精化从形式化到半自动化的发展  

Mutually-Inversistic Program Refinement :Formal to Semiautomatic Development of the Refinement

作　　者：周训伟 鲍泓[1] 

机构地区：[1]北京联合大学信息技术研究所,北京,100101 北京联合大学信息学院,北京,100101

出　　处：《计算机工程与科学》2006年第z2期161-162,共2页Computer Engineering & Science

摘　　要：Carroll Morgan的规则精化方法是一种典型的程序精化方法,是一种形式方法.本文用互逆主义逻辑对其进行了改造:将其中的精化法则改造成为逻辑定理,以二层假言推理和小前提逆二层单准正向证明系统为推理规则,使得程序精化从形式化发展为半自动化.

关 键 词：互逆主义逻辑 程序精化 精化定理 规范 代码 

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