已驗證的軟件工具鏈：if-then-else proof

我正在學習使用Verified Software Toolchain（VST）。我被困在證明一個簡單的「if-then-else」塊。已驗證的軟件工具鏈：if-then-else proof

這裏是.c文件：

int iftest(int a){ 
    int r=0; 
    if(a==2){ 
     r=0; 
    else{ 
     r=0; 
    } 
return r; 
}

我寫一個關於iftest()如下規格：

Definition if_spec :=` 
DECLARE _iftest` 
     WITH a0:int 
       PRE [_a OF tint] 
       PROP() 
       LOCAL (`(eq (Vint a0)) (eval_id _a)) 
       SEP() 
       POST [tint] 
       PROP() 
       LOCAL ((`(eq (Vint (Int.repr 0))) retval)) 
       SEP().`

的證明步驟是：

Lemma body_iftest : semax_body Vprog Gtot f_iftest if_spec.Proof. start_function. name a _a. name r _r. forward. (*r=0*) simplify_typed_comparison. forward. (*if(E)*). go_lower. subst. normalize.

它產生一個假設：Post := EX x : ?214, ?215 x : environ -> mpred並且「then」子句不能通過「go_lower」和「normalize」繼續。

來源

2013-08-20 lgbo

我從來沒有使用過VST（實際上這是我第一次聽說它）。您可能會在自己的郵件列表或Coq郵件列表中獲得更多反饋：https：//sympa.inria.fr/sympa/arc/coq-club。 – Vinz

@Vinz VST現在還沒有郵件列表，但他們最近爲SO – Necto

可能是一個沒有幫助的答案，但我不禁注意到你的.c代碼有3個{和只有2個}，暗示它不能編譯。您收到的錯誤消息是否與此有關？

來源

2013-08-27 22:10:11 bazza

上的問題創建了一個標籤'verifiable-c'是的，他錯過了「else」之前的「}」。隨着增加，該函數歸結爲返回0，所以我不完全確定它的任何點。我猜他快速地打出了一個捏造的例子，並且現在有一些錯誤。 –

在當前版本的VST中有一個forward_if PRED策略。以下是您如何使用它來解決您的目標：

Require Import floyd.proofauto. 
Require Import iftest. 

Local Open Scope logic. 
Local Open Scope Z. 

Definition if_spec := 
    DECLARE _iftest 
     WITH a0:int 
       PRE [_a OF tint] 
       PROP() 
       LOCAL (`(eq (Vint a0)) (eval_id _a)) 
       SEP() 
       POST [tint] 
       PROP() 
       LOCAL ((`(eq (Vint (Int.repr 0))) retval)) 
       SEP(). 

Definition Vprog : varspecs := nil. 
Definition Gtot : funspecs := if_spec :: nil. 

Lemma body_iftest : semax_body Vprog Gtot f_iftest if_spec. 
Proof. 
    start_function. 
    name a _a. 
    name r _r. 
    forward. 
    forward_if (PROP() 
        LOCAL (`(eq (Vint (Int.repr 0))) (eval_id _r)) SEP()). 
    + forward. 
    entailer. 
    + forward. 
    entailer. 
    + forward. 
Qed.

P.S. @bazza對else之前的}是錯的。我認爲它是固定的。

來源

2015-01-11 18:24:42 Necto

已驗證的軟件工具鏈：if-then-else proof

回答

相關問題