软件导刊
軟件導刊
연건도간
SOFT WARE GUIDE
2014年
6期
9-10
,共2页
Hoare公理%正确性验证%WP语义%公理化方法%前置条件
Hoare公理%正確性驗證%WP語義%公理化方法%前置條件
Hoare공리%정학성험증%WP어의%공이화방법%전치조건
随着软件规模越来越大，软件正确性问题也随之而来，基于 Hoare公理系统的程序形式化验证方法，能够保证并提高软件的正确性。针对 Hoare公理化方法证明中的前置条件难以寻找的问题，利用最弱前置变换法求出前置谓词作为公理化方法的前置条件。
隨著軟件規模越來越大，軟件正確性問題也隨之而來，基于 Hoare公理繫統的程序形式化驗證方法，能夠保證併提高軟件的正確性。針對 Hoare公理化方法證明中的前置條件難以尋找的問題，利用最弱前置變換法求齣前置謂詞作為公理化方法的前置條件。
수착연건규모월래월대，연건정학성문제야수지이래，기우 Hoare공리계통적정서형식화험증방법，능구보증병제고연건적정학성。침대 Hoare공이화방법증명중적전치조건난이심조적문제，이용최약전치변환법구출전치위사작위공이화방법적전치조건。
