程序验证的一个逻辑系统

【摘要】 <正> 程序证明系统是形式化的基于一些公理和推论法则的逻辑系统.这些系统的完全性问题,一直引起人们的广泛注意.已经知道,当程序语言具有足够强的表达能力时,Hoare证明系统是不完全的.近几年来,国内外许多学者致力于建立一个完全的证明系统,但到目前为止,得到的基本上是相对完全性的结果.更多还原