程序设计方法学(下)

【摘要】 <正> 十、程序的形式推导技术10.1 程序的形式语义程序变量的一组可能取值,称为是一个状态,Hoare公式{P}S{θ}的前谓词P和后谓词Q分別确定了程序S执行的初始状态和终结状态所需满足的条件,因此,可以说,这种谓词刻画了程序语言结构的语义特征。然而,前谓词P确定的只是一个充分条件,以满足前谓词P的程序状态作为初始状态,执行程序S,导致的结果状态必然满足Q更多还原