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