1

ACSL で定義された帰納述語で帰納を使用することは可能ですか?

ACSL マニュアルの次の例を検討してください。

struct List {
    int value;
    struct List* next;
};
/*@ inductive reachable{L}(struct List* root, struct List* to) {
  @   case empty{L}: \forall struct List* l; reachable(l, l);
  @   case non_empty{L}: \forall struct List *l1,*l2;
  @     \valid(l1) && reachable(l1->next, l2) ==> reachable(l1, l2);
  @ }
*/

次の補題を証明しようとしています。

/*@ lemma next_null_reachable: \forall struct List* l;
  @   \valid(l) && reachable(l, \null) ==> reachable(l->next, \null);
*/

Alt-Ergo はここで失敗するので、手動の Coq 推論に頼ります。

Goal
  forall (t : array Z),
  forall (t_1 : farray addr addr),
  forall (a : addr),
  ((valid_rw t a 2%Z)) ->
  ((P_reachable t t_1 a (null))) ->
  ((P_reachable t t_1 (t_1.[ (shiftfield_F_List_next a) ]) (null))).

しかし、 Iの場合Search P_reachable、次の 2 つの公理のみが生成されていることがわかります。

Q_non_empty:
  forall (t : array int) (t_1 : farray addr addr) (a_1 a : addr),
  valid_rw t a_1 2 ->
  P_reachable t t_1 (t_1 .[ shiftfield_F_List_next a_1]) a ->
  P_reachable t t_1 a_1 a
Q_empty:
  forall (t : array int) (t_1 : farray addr addr) (a : addr),
  P_reachable t t_1 a a

そして誘導原理はありません。だから応募できないinduction P_reachableとかdestruct P_reachable。

frama-cバージョン Sodium-20150201の WP プラグインを使用しています。

再現するには、との定義と補題frama-c -wp -wp-rte -wp-prover coqide file.cがfile.c含まれているを実行できます。Listreachablenext_null_reachable

4

2 に答える 2

2

あなたの目標の形から、WP プラグインを使用していると思います。実際、 が と の 2 つのケースをreachable検証する最小の述語であることを示す補題は提供されません。つまり、帰納法を使用できないことを意味します。emptynon_empty

私の記憶が正しければ、そのような公理を追加すると、一階定理の証明者を混乱させることになります (reachableスルーemptyまたはnon_empty帰納法のインスタンスを繰り返し構築し、それらを破壊します)。ただし、WP の Coq 出力は、完全な翻訳を提供できます。

回避策は、帰納原理の代わりに (WP では証明できない) 特殊な補題の適切なセットを提供することです。たとえばbinary_search_proved.c、このアーカイブを参照してください。

于 2015-09-08T12:28:15.663 に答える