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

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