论文部分内容阅读
首先给出了量子最弱自由前置条件（weakest liberal precondition,简称wlp）wlp （A,B,C）-可交换的定义,研究了wlp （A,B,C）-可交换的充分必要条件;其次,得到了wlp 不是良好的谓词转换,验证了wlp 是比量子最弱前置条件（weakest precondition,简称wp）更弱的谓词转换,揭示了wlp 和wp 的本质区别;最后证明了wlp 的序列合成、并行合成和块结构等性质.