當前位置:首頁 > 科技文檔 > 數(shù)學 > 正文

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

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

開通會員,享受整站包年服務立即開通 >