健康模糊谓词转换器

• 作 者: 吴恒洋 马艳芳
• 机 构: 上海师范大学数理信息学院,上海,200234
• 出 处: 中国系统工程学会模糊数学与模糊系统专业委员会第十三届年会
• 发表日期: 2006年10期
• 关键词: 模糊谓词 转换器 程序语言 语义

谓词转换器语义是使用程序验证技术来定义程序语言的一种方法.传统的谓词转换器语义是由Dijkstra通过最弱前置条件给出的,后来Kozen把它推广到概率谓词转换器.在2001年陈仪香与Achim Jung提出了模糊谓词转换器的概念,并给出了三种模糊谓词转换器.最近陈仪香和Plotkin提出了健康模糊谓词转换器的概念.本文主要讨论健康模糊谓词转换器的性质,主要结论是:(1)从Pf(E)到Pf(D)所有健康模糊谓词转换器在点式序下构成一个cpo;(2)健康模糊谓词转换器关于线性运算是封闭的.