一种程序推导与验证方法研究

随着软件规模越来越大,软件正确性问题也随之而来,基于Hoare公理系统的程序形式化验证方法,能够保证并提高软件的正确性。针对Hoare公理化方法证明中的前置条件难以寻找的问题,利用最弱前置变换法求出前置谓词作为公理化方法的前置条件。