命令式動態(tài)規(guī)劃類算法程序推導(dǎo)及機械化驗證

摘要： 動態(tài)規(guī)劃是一種遞歸求解問題最優(yōu)解的方法,主要通過求解子問題的解并組合這些解來求解原問題.由于其子問題之間存在大量依賴關(guān)系和約束條件,所以驗證過程繁瑣,尤其對命令式動態(tài)規(guī)劃類算法程序正確性驗證是一個難點.基于動態(tài)規(guī)劃類算法Isabelle/HOL函數(shù)式建模與驗證,通過證明命令式動態(tài)規(guī)劃類算法程序與其的等價性,避免證明正確性時處理復(fù)雜的依賴關(guān)系和約束條件,提出命令式動態(tài)規(guī)劃類算法程...