當(dāng)前位置:首頁(yè) > 科技文檔 > 數(shù)學(xué) > 正文

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

軟件學(xué)報(bào) 頁(yè)數(shù): 24 2024-04-28
摘要: 動(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)算法程...

開(kāi)通會(huì)員,享受整站包年服務(wù)立即開(kāi)通 >
科技文檔
數(shù)學(xué) 力學(xué) 化學(xué) 金融 證券 保險(xiǎn) 投資 會(huì)計(jì) 審計(jì) 園藝 林業(yè) 旅游 體育 物理學(xué) 生物學(xué) 天文學(xué) 氣象學(xué) 海洋學(xué) 地質(zhì)學(xué) 新能源 金屬學(xué) 農(nóng)藝學(xué) 農(nóng)作物 管理學(xué) 領(lǐng)導(dǎo)學(xué) 自然科學(xué) 系統(tǒng)科學(xué) 資源科學(xué) 無(wú)機(jī)化工 有機(jī)化工 燃料化工 化學(xué)工業(yè) 材料科學(xué) 礦業(yè)工程 冶金工業(yè) 安全科學(xué) 環(huán)境科學(xué) 工業(yè)通用 機(jī)械工業(yè) 無(wú)線(xiàn)電子 電信技術(shù) 鐵路運(yùn)輸 汽車(chē)工業(yè) 船舶工業(yè) 動(dòng)力工程 電力工業(yè) 農(nóng)業(yè)科學(xué) 農(nóng)業(yè)工程 植物保護(hù) 動(dòng)物醫(yī)學(xué) 教育理論 學(xué)前教育 初等教育 中等教育 高等教育 職業(yè)教育 成人教育 自然地理 地球物理 經(jīng)濟(jì)統(tǒng)計(jì) 農(nóng)業(yè)經(jīng)濟(jì) 工業(yè)經(jīng)濟(jì) 交通經(jīng)濟(jì) 企業(yè)經(jīng)濟(jì) 文化經(jīng)濟(jì) 信息經(jīng)濟(jì) 貿(mào)易經(jīng)濟(jì) 財(cái)政稅收 市場(chǎng)研究 科學(xué)研究 互聯(lián)網(wǎng) 自動(dòng)化 輕工業(yè) 核科學(xué) 服務(wù)業(yè) 石油然氣 服務(wù)業(yè) 野生動(dòng)物 水產(chǎn)漁業(yè) 硬件 儀器儀表 航空航天 武器軍事 公路運(yùn)輸 水利水電 建筑科學(xué) 軟件