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

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