论文部分内容阅读
基于Tableau方法的z规格说明求精以定理证明为基础,将从规格说明得到程序的过程看作是一个定理证明的过程,如果这个证明存在,那么从证明中可抽取出一个满足该程序规格说明的程序.本文引进合并规则扩充Tableau方法的演绎规则,并利用该规则给出了Z语言中模式的与、或操作的求精方法,从而简化了模式复合的求精;为了使Tableau方法能够用于Z规格说明的求精,我们将Z语言的结构成分转化为Tableau方法所能接受的结构.