填空题 程序正确性证明最常用的方法是 __ 1__ ，它对程序提出一组命题。如果在数学上证明这些命题成立，就能保证程序不发生错误。