第7章程序驗證-資料下載頁
2025-08-23 09:06本頁面
【導讀】循環(huán)不變式的推斷。以GeeC.Necula教授的講稿為主來介紹。Hoare邏輯的良形公式。Hoare邏輯良形公式{P}C{Q}的解釋。結(jié)果狀態(tài)一定滿足Q。部分正確性的證明規(guī)則。P在謂詞邏輯的自然演繹演。–變成計算WP(C,Q)并且證明P?–即使得到了WP(C,Q)，檢查蘊涵P?–對于循環(huán)語句怎么辦？
【正文】 ? (y ? n) (x+m = m?(y+1)) ? ((y+1) ? n) x = x + m 。 (x = m?(y+1)) ? ((y+1) ? n) y = y + 1 。 } ((x = m?y) ? (y ? n)) ? ?(y n) ? (x = m?n) } x = m ? n 第 2個驗證條件 驗證條件生成 n ? 0 function mult(m, n){ x = 0 。 (x = m?0) ? (0 ? n) y = 0 。 ((x = m?y) ? (y ? n)) ? (y n) ? (x+m = m?(y+1)) ? ((y+1) ? n) while y n do { (x = m?y) ? (y ? n) (x+m = m?(y+1)) ? ((y+1) ? n) x = x + m 。 (x = m?(y+1)) ? ((y+1) ? n) y = y + 1 。 } ((x = m?y) ? (y ? n)) ? ?(y n) ? (x = m?n) } x = m ? n 驗證條件生成 n ? 0 function mult(m, n){ (0 = m?0) ? (0 ? n) x = 0 。 (x = m?0) ? (0 ? n) y = 0 。 ((x = m?y) ? (y ? n)) ? (y n) ? (x+m = m?(y+1)) ? ((y+1) ? n) while y n do { (x = m?y) ? (y ? n) (x+m = m?(y+1)) ? ((y+1) ? n) x = x + m 。 (x = m?(y+1)) ? ((y+1) ? n) y = y + 1 。 } ((x = m?y) ? (y ? n)) ? ?(y n) ? (x = m?n) } x = m ? n 驗證條件生成 n ? 0 function mult(m, n){ ( n ? 0 ) ? ((0 = m?0) ? (0 ? n)) (0 = m?0) ? (0 ? n) x = 0 。 (x = m?0) ? (0 ? n) y = 0 。 ((x = m?y) ? (y ? n)) ? (y n) ? (x+m = m?(y+1)) ? ((y+1) ? n) while y n do { (x = m?y) ? (y ? n) (x+m = m?(y+1)) ? ((y+1) ? n) x = x + m 。 (x = m?(y+1)) ? ((y+1) ? n) y = y + 1 。 } ((x = m?y) ? (y ? n)) ? ?(y n) ? (x = m?n) } x = m ? n 第 3個驗證條件 驗證條件生成 n ? 0 function mult(m, n){ ( n ? 0 ) ? ((0 = m?0) ? (0 ? n)) x = 0 。 y = 0 。 ((x = m?y) ? (y ? n)) ? (y n) ? (x+m = m?(y+1)) ? ((y+1) ? n) while y n do { (x = m?y) ? (y ? n) x = x + m 。 y = y + 1 。 } ((x = m?y) ? (y ? n)) ? ?(y n) ? (x = m?n) } x = m ? n 這三個驗證條件需要證明
教學課件相關推薦
鄂ICP備17016276號-1