摘要
基于Hoare逻辑,给出了概率拟Hoare逻辑,用于刻画程序执行的正确度,定量地描述理论与程序(或软件)实际执行之间的差距,反映理论被程序实现的程度,从而量化理论上正确的程序在实际执行时出错的可能性,以及解释正确度很高的两个程序串行复合之后的整体正确度可能并不高等问题。
A Hoare logic-baesed probabilistic quasi-Hoare logic for program correctness assessment was presented. Probabilistic quasi-Hoare logic describes the difference between the theory idea and implementation, and reflects the de- gree of which the theory idea is implemented by the program in practice. Thus, it can formally explain the reasons of er- rors of programs which are theoretically correct and the low correctness degree of the sequential composition of two programs （components） which are both high in correctness degree, etc.
出处
《计算机科学》
CSCD
北大核心
2016年第4期177-181,191,共6页
Computer Science
