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