完全相容稳定模糊谓词转换器

谓词转换器语义是用程序验证技术来定义程序语言的一种方式。为描述程序的语义,在稳定模糊谓词的基础上建立完全相容稳定模糊谓词转换器,讨论完全相容稳定模糊谓词转换器的拓扑语义。同时给出它与状态转换器之间的一个保序关系,说明完全相容稳定模糊谓词转换器一定是状态转换器。