健康模糊谓词转换器

摘要：

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

关键词： 模糊谓词 转换器 程序语言 语义

作者: 吴恒洋 马艳芳

作者单位: 上海师范大学数理信息学院,上海,200234

会议类型: 国内会议

会议名称: 中国系统工程学会模糊数学与模糊系统专业委员会第十三届年会

会议地点: 西安

会议语种:中文

页码: 340-343

在线出版日期: 2006-10-01（万方平台首次上网日期，不代表论文的发表时间）