scopelogic工具研究進展(已修改)
2024-10-28 15:03 本頁面
【正文】 Scope Logic工具研究進展 趙建 華 南京大學(xué)計算機系 蘇州 目錄 ? Scope Logic介紹 ? 工具介紹 – 基本框架介紹 – 公式的分類 – 公式的狀態(tài) – 證明公式的基本方式 – 自動化 ? 未來的工作 Scope Logic介紹（ 1） Scope Logic介紹（ 2） Scope Logic介紹（ 3） if(ab) Assert i: {…..} a = a – b Assert j: {a = a@i b} … 工具的基本框架 ? 交互式證明工具，支持一定程度的自動化 ? 使用 Proof In Code的方式證明程序 – 允許用戶自定義函數(shù)，函數(shù)的內(nèi)存范圍函數(shù)、以及這些函數(shù)具有的性質(zhì)（工具不保證這些函數(shù)的正確性） – 公式被寫在不同的程序點上， – 一個程序點上可以有多個公式 – 通過漸進的方式證明程序 – 使用 SMT Solver Z3進行程序點內(nèi)部的公式推導(dǎo) 工具的界面 公式的分類 ? 強制 公式 – 必須證明的公式，以防止零除、數(shù)組越界、空指針引用、 … – 由工具在打開源程序時自動添加 ? 自 生公式 – 必然成立的公式，包括 if/while語句的 conditions，賦值語句之后的等式等 – 部分由工具直接添加，部分由用戶輸入 ? 用戶輸入的公式 公式的狀態(tài) ? 由工具或用戶插入的公式有兩種狀態(tài) – 待證明 ：公式輸入后尚未 證明 – 已證明：該公式已經(jīng)可以由其它公式作為依據(jù)證明。 ? 可以 依賴于待證明的 公式，所以已證明的公式未必成立 ? 如果它依賴的公式被刪除 /修改，則該公式會重新變成待證明狀態(tài) ? 在程序入口處的公式可以看作前置條件，不需要證明。 ? 當(dāng)一個程序中所有的公式都處于證明狀態(tài)時，這些公式就都確定成立了 公式的證明方式 ? 自生 – 只要程序運行到程序點 i，該公式一定成立 – 注：在賦值 /Alloc語句之后的自生公式證明略有變化 ? 傳播 – 公式 p在程序點上成立是因為 p在其他程序點上成立 ? @證明 – p可以由同一程序點 i上的公式 p’加上一些 @i而得到 ? 推導(dǎo) – 一 個公式可以由同一個程序點上的公式推導(dǎo)得到 自生公式證明 傳播證明（ if） ? if語句 – P在 if語句之前成立，則在兩個分支之前都成立 – P在兩個分支之后都成立，則在 if語句之后成立 ? 操作： – 在 if之前的公式 P被拷貝到兩個分支之前 ?
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號-1