验证的软件工具链: if-then-else证明

Question

我正在学习使用经过验证的软件工具链(VST)。我被困在证明一个简单的"if-then-else“代码块上。

下面是.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“继续。

Answer 1

在当前版本的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.

另外，在else之前，@bazza关于}丢失的说法是对的。我想它已经修好了。

Answer 2

这可能是一个没有帮助的答案，但我不禁注意到你的.c代码有3个{而只有2个}，这表明它无法编译。你收到的错误消息会不会与此有关？