量子计算研究主要有物理学家和计算机科学家两支力量,前者关注的是量子计算的物理实现,后者关注的是量子程序设计语言的理论和实现.而程序验证是保证程序正确性的关键技术.如基于逻辑推理的验证,最著名的就是霍尔(Hoare)逻辑;模型检验主要针对可归结为有限状态的程序.量子通讯比经典通讯最突出的优点就是它的安全性.然而,量子通讯协议在设计阶段要想保证它的正确性是相当困难的.由于量子系统与经典系统相比有许多本质不同的特征,如量子信息的不可克隆性、纠缠的存在等,因而经典的软件理论、方法和技术在很大程度上不能直接适用于量子软件,这使得量子软件的研究成为一个十分困难而富有挑战性的课题.终止条件、时间和空间复杂性研究是循环程序研究的一个重要而非常困难的问题.事实上一般量子循环的终止是不可判定的.本论文主要围绕由量子信道构成的量子程序的终止条件、广义量子loop程序的终止条件、非确定型量子程序的终止条件及推理量子霍尔(Hoare)逻辑的最弱自由前置条件语义等几个方面进行讨论,这些结果都是对量子程序验证理论的有益完善.文章的主要工作包括以下几个方面：(1)量子程序终止的研究：运用量子程序验证方法通过选取不同的可观测算子,讨论了单量子比特系统上比特翻转、去极化、幅值阻尼、相位阻尼等信道刻画的量子程序的终止情况.研究表明：由这些量子信道所描述的量子程序的终止不仅依赖于输入态的选取,而且还依赖于可观测算子的选取.该内容见第三章.(2)广义量子loop程序终止的研究：当广义量子loop程序(generalized quan-tum loop program,简记为GQLoop)的主体由比特翻转、去极化、幅值阻尼、相位阻尼等信道描述时,讨论了GQLoop程序终止(几乎终止)的情况及两类GQLoop程序相互嵌套时loop程序的终止(几乎终止)等问题.研究表明：以量子运算的嵌套为主体的GQLoop程序终止(几乎终止)的条件依赖于刻画量子信道的参数.当开放量子系统与其环境在酉运算下做为loop程序的主体时,讨论了在酉运算后去掉环境时的主系统上量子程序的执行过程.该内容见第四章.(3)非确定型量子程序终止的研究：首先讨论了单量子比特空间中比特翻转、相位翻转、去极化、幅值阻尼、相位阻尼等信道作为特殊的非确定型量子程序-确定型量子程序,从计算基态运行时的可达集合、发散集合及终止情况.其次,详细讨论了这五种信道分类两两组成的非确定型量子程序从计算基态运行时的可达集合、发散集合及终止情况.研究表明：由五种常用信道分类两两组成的非确定型量子程序的终止情况比较复杂,有的依赖于刻画量子信道的两个参数,有的与刻画量子信道的两个参数没有关系.最后,研究了C3和C4空间中由两个量子游走程序组成的非确定型量子程序的可达集合、发散集合及终止情况.研究表明：非确定型量子程序的可达集合、发散集合及终止与选取的测量算子有密切的联系.程序在不同测量算子作用下从同一个初态运行时可能终止,也可能发散；同一个初态的可达集合中终态与发散态共存.该内容见第五章.(4)最弱自由前置条件语义的研究：提出了量子最弱自由前置条件(weak-est liberal precondition,简记为wlp)wlp(A,B,C)-可交换的定义,研究了wlp(A,B,C)-可交换的充分必要条件,得到了wlp不是良好的谓词转换,验证了wlp是比量子最弱前置条件(weakest precondition,简记为wp)更弱的谓词转换,揭示了wlp和wp的本质区别.给出了wlp的序列合成、并行合成和块结构等性质,讨论了＆算子的一些运算性质,这些性质对我们理解和研究wp和wlp很有帮助.该内容见第六章.