3

検証済みソフトウェア ツールチェーン (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」によって続けることはできません。

4

2 に答える 2

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.

PS @bazza は、}beforeの欠落について正しいelseです。私はそれが修正されたと仮定します。

于 2015-01-11T18:24:42.910 に答える
0

役に立たない答えになる可能性がありますが、.c コードに { が 3 つあり、} が 2 つしかなく、コンパイルされていないことを示唆していることに気付かずにはいられません。表示されているエラー メッセージに何か関係があるのでしょうか?

于 2013-08-27T22:10:11.150 に答える