如何在函数规范中使用超过 8 个变量？

Question

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（2014 年 1 月）和 OCaml 4.01.0。

Answer 1

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

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).

Answer 2

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

如何在函数规范中使用超过 8 个变量？

How to use more than 8 variables in a function specification?

verifiable-c