1

WITH构造只为最多 8 个变量定义。如何使用超过 8 个？例子：

Definition find_key_spec :=
  DECLARE _find_key
    WITH sh : share, m : ArrMapZ, start : Z, key : Z, i : nat,
         vbb : val, vkeys : val, vstart : val, vkey : val, vi : val
    PRE ...

=>

Toplevel input, characters 176-177:
Syntax error: 'PRE' '[' expected after [constr:operconstr level 200]
(in [constr:binder_constr]).

我使用：VST 1.5（2014-10-02 时为 6834P）、CompCert 2.4、Coq 8.4pl3（Jan'14）和 OCaml 4.01.0。

4

2 回答 2

1

WITH我的解决方案：用 10 个变量定义符号：

Notation "'WITH'  x1 : t1 , x2 : t2 , x3 : t3 , x4 : t4 , x5 : t5 ,
                  x6 : t6 , x7 : t7 , x8 : t8 , x9 : t9 , x10 : t10
                  'PRE'  [ u , .. , v ] P 'POST' [ tz ] Q" :=
     (mk_funspec ((cons u%formals .. (cons v%formals nil) ..), tz)
                 (t1*t2*t3*t4*t5*t6*t7*t8*t9*t10)
           (fun x => match x with (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) =>
                                  P%logic end)
           (fun x => match x with (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) =>
                                  Q%logic end))
            (at level 200, x1 at level 0, x2 at level 0, x3 at level 0,
                           x4 at level 0, x5 at level 0, x6 at level 0,
                           x7 at level 0, x8 at level 0, x9 at level 0,
                           x10 at level 0, P at level 100, Q at level 100).
于 2015-01-24T12:51:08.027 回答
1

另一种方法是在 WITH 子句中引入元组（例如 WITH x12: (t1 * t2)%type），并通过投影在 PRE 和 POST 中引用它们的组件（例如，使用 fst x12 代替 PRE 中的 x1）。

于 2015-01-26T19:18:37.563 回答