Research Space for Linear Algebra & Discrete Mathematics
因為這題應該算是屬於軟工或是logic inference的部份, 離散一般不會考到這個範圍, 所以我下面寫的你可以參考看看就好題目裡的WP指的是Hoare logic裡的weakest precondition, 符號WP(S,R)大概的意思是, S搜集程式裡的一些commands, R則是一個述詞, 一般稱為postcondition, 你可以把它想成是程式執行到最後的結果, 也就是說在給定postcondition R之下我們希望去推出他的precondition為何, 而因為這樣推出來的precondition會是符合邏輯結果的最基本要求, 所以我們稱它為weakest precondition, 譬如取 S 為 x:=y-1, R 為 x>0, 則 WP(S,R) = (y-1>0) = (y>1)WP通常可用一些已知的inference rule來做嚴謹的逐步化簡, 不過這裡我想你也可以用一些邏輯的分析來simplify它, 我推出來的結果是(1) (x=y-v)∧(y＞0)(2) (u=2)∧(v=2)(3) ((y＜0)∧(u＜-2)) ∨ ((0≦y＜5)∧(u＜-6))第(1),(2)題還好, 但像是第(3)題就比較難處理, 細節及步驟可能要麻煩你自己驗證了
助教到底唸什麼系阿~?什麼都會解@@
謝謝助教
張貼留言
3 則留言:
因為這題應該算是屬於軟工或是logic inference的部份, 離散一般不會考到這個範圍, 所以我下面寫的你可以參考看看就好
題目裡的WP指的是Hoare logic裡的weakest precondition, 符號WP(S,R)大概的意思是, S搜集程式裡的一些commands, R則是一個述詞, 一般稱為postcondition, 你可以把它想成是程式執行到最後的結果, 也就是說在給定postcondition R之下我們希望去推出他的precondition為何, 而因為這樣推出來的precondition會是符合邏輯結果的最基本要求, 所以我們稱它為weakest precondition, 譬如取 S 為 x:=y-1, R 為 x>0, 則 WP(S,R) = (y-1>0) = (y>1)
WP通常可用一些已知的inference rule來做嚴謹的逐步化簡, 不過這裡我想你也可以用一些邏輯的分析來simplify它, 我推出來的結果是
(1) (x=y-v)∧(y＞0)
(2) (u=2)∧(v=2)
(3) ((y＜0)∧(u＜-2)) ∨ ((0≦y＜5)∧(u＜-6))
第(1),(2)題還好, 但像是第(3)題就比較難處理,
細節及步驟可能要麻煩你自己驗證了
助教到底唸什麼系阿~?
什麼都會解@@
謝謝助教
張貼留言