scopelogic工具研究進(jìn)展-資料下載頁(yè)
2025-10-03 15:03本頁(yè)面
【導(dǎo)讀】交互式證明工具，支持一定程度的自動(dòng)化。使用ProofInCode的方式證明程序。–必然成立的公式，包括if/while語(yǔ)句的conditions，由工具或用戶插入的公式有兩種狀態(tài)。如果它依賴的公式被刪除/修改，則該公式會(huì)重新變成待證明。在程序入口處的公式可以看作前置條件，不需要證。這兩個(gè)公式已證明，且依賴于原來(lái)的p. 僅當(dāng)確認(rèn)P是循環(huán)不變式時(shí)才可以傳播。自動(dòng)判斷p能否由同assert中某公式加@i而得到。只在同程序點(diǎn)上的公式之間進(jìn)行。簡(jiǎn)單的涉及取地址運(yùn)算的公式證明和簡(jiǎn)化。基本塊內(nèi)部的證明。完成常見(jiàn)遞歸數(shù)據(jù)結(jié)構(gòu)的遞歸函數(shù)和性質(zhì)。開(kāi)放數(shù)據(jù)流分析的接口，增加更多數(shù)據(jù)流。支持局部推導(dǎo)和過(guò)程調(diào)用
【正文】 ) while (a0 amp。amp。 b0) { ASSERT2( ) if(ab) ASSERT3( P： ab。 ) a = a – (b/a)*a。 ASSERT4( ) else ASSERT5( ) b = b – (a/b)*b。 ASSERT6( ) ASSERT7( ) } ASSERT7( ) Q： a@3b //依賴于 P推導(dǎo) ? 只在同程序點(diǎn)上的公式之間進(jìn)行 ? 使用 SMT Solver Z3完成 輔助的自動(dòng)化功能 ? @證明方式 ? 簡(jiǎn)單的涉及取地址運(yùn)算的公式證明和簡(jiǎn)化 ? 基本 塊內(nèi)部的證明 – 在受限條件下，能夠在基本塊入口處生成公式的前置條件 ? 數(shù)據(jù)流分析 – 整數(shù)變量 的取值范圍 – 空 指針?lè)治? – 單 鏈表分析 將來(lái)的工作 ? 完成常見(jiàn)遞歸數(shù)據(jù)結(jié)構(gòu)的遞歸函數(shù)和性質(zhì)的定義 – 單鏈表，雙向鏈表，二叉樹(shù) ? 開(kāi)放數(shù)據(jù)流分析的接口，增加更多數(shù)據(jù)流分析功能 ? 基于模式的自動(dòng)證明方式 ? 支持局部推導(dǎo)和過(guò)程調(diào)用 謝謝
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號(hào)-1