如何对持有 return 值的变量使用 retval-postcondition?
How to use retval-postcondition on a variable holding the return value?
我的简单程序是vars.c
:
int pure0 ()
{
return 0;
}
int get0(int* arr)
{
int z = pure0();
return z;
}
我开始证明(文件verif_vars.c
):
Require Import floyd.proofauto.
Require Import vars.
Local Open Scope logic.
Local Open Scope Z.
Definition get0_spec :=
DECLARE _get0
WITH sh : share, arr : Z->val, varr : val
PRE [_arr OF (tptr tint)]
PROP ()
LOCAL (`(eq varr) (eval_id _arr);
`isptr (eval_id _arr))
SEP (`(array_at tint sh arr 0 100) (eval_id _arr))
POST [tint] `(array_at tint sh arr 0 100 varr) &&
local(`(eq (Vint (Int.repr 0))) retval).
Definition pure0_spec :=
DECLARE _pure0
WITH sh : share
PRE []
PROP ()
LOCAL ()
SEP ()
POST [tint] local(`(eq (Vint (Int.repr 0))) retval).
Definition Vprog : varspecs := nil.
Definition Gprog : funspecs := get0_spec :: pure0_spec ::nil.
Lemma body_pure0: semax_body Vprog Gprog f_pure0 pure0_spec.
Proof.
start_function.
forward.
Qed.
Lemma body_get0: semax_body Vprog Gprog f_get0 get0_spec.
Proof.
start_function.
name arrarg _arr.
name zloc _z.
name zloc' _z'.
forward_call (sh).
entailer!.
auto with closed.
after_call.
forward.
entailer!.
最后有两个子目标:
Espec : OracleKind
sh : share
arr : Z -> val
Struct_env := abbreviate : type_id_env.type_id_env
Delta := abbreviate : tycontext
zloc0 : val
arrarg : val
zloc : int
TC : is_pointer_or_null arrarg
Parrarg : isptr arrarg
============================
Int.repr 0 = zloc
subgoal 2 (ID 1273) is:
!!(Int.repr 0 = zloc) |-- emp
- 第一个直接来自
pure0_spec
后置条件。但是我怎么能告诉 Coq 呢?
- 第二个目标可以简化(
admit. entailer.
)为TT |-- emp
。这似乎又是微不足道的,而且如何证明它(SearchAbout derives
和 SearchAbout emp
没有显示任何一般引理)?
我使用:VST 1.5(2014-10-02 时为 6834P)、CompCert 2.4、Coq 8.4pl3(2014 年 1 月)和 OCaml 4.01.0。
首先:副手,我自己没有尝试重现这一点——是否有可能使用 entailer!
也太 "risky",因为(如文档所述)entailer!
有时可以证明目标变成一个无法证明的目标。试试不带刘海的 entailer
,看看会不会更好看。
其次,TT |-- emp
不成立。 TT
适用于任何堆,emp
只适用于空堆。您可以通过将 pure
函数的后置条件更改为
来解决此问题
POST [tint] local(`(eq (Vint (Int.repr 0))) retval) && emp.
我的简单程序是vars.c
:
int pure0 ()
{
return 0;
}
int get0(int* arr)
{
int z = pure0();
return z;
}
我开始证明(文件verif_vars.c
):
Require Import floyd.proofauto.
Require Import vars.
Local Open Scope logic.
Local Open Scope Z.
Definition get0_spec :=
DECLARE _get0
WITH sh : share, arr : Z->val, varr : val
PRE [_arr OF (tptr tint)]
PROP ()
LOCAL (`(eq varr) (eval_id _arr);
`isptr (eval_id _arr))
SEP (`(array_at tint sh arr 0 100) (eval_id _arr))
POST [tint] `(array_at tint sh arr 0 100 varr) &&
local(`(eq (Vint (Int.repr 0))) retval).
Definition pure0_spec :=
DECLARE _pure0
WITH sh : share
PRE []
PROP ()
LOCAL ()
SEP ()
POST [tint] local(`(eq (Vint (Int.repr 0))) retval).
Definition Vprog : varspecs := nil.
Definition Gprog : funspecs := get0_spec :: pure0_spec ::nil.
Lemma body_pure0: semax_body Vprog Gprog f_pure0 pure0_spec.
Proof.
start_function.
forward.
Qed.
Lemma body_get0: semax_body Vprog Gprog f_get0 get0_spec.
Proof.
start_function.
name arrarg _arr.
name zloc _z.
name zloc' _z'.
forward_call (sh).
entailer!.
auto with closed.
after_call.
forward.
entailer!.
最后有两个子目标:
Espec : OracleKind
sh : share
arr : Z -> val
Struct_env := abbreviate : type_id_env.type_id_env
Delta := abbreviate : tycontext
zloc0 : val
arrarg : val
zloc : int
TC : is_pointer_or_null arrarg
Parrarg : isptr arrarg
============================
Int.repr 0 = zloc
subgoal 2 (ID 1273) is:
!!(Int.repr 0 = zloc) |-- emp
- 第一个直接来自
pure0_spec
后置条件。但是我怎么能告诉 Coq 呢? - 第二个目标可以简化(
admit. entailer.
)为TT |-- emp
。这似乎又是微不足道的,而且如何证明它(SearchAbout derives
和SearchAbout emp
没有显示任何一般引理)?
我使用:VST 1.5(2014-10-02 时为 6834P)、CompCert 2.4、Coq 8.4pl3(2014 年 1 月)和 OCaml 4.01.0。
首先:副手,我自己没有尝试重现这一点——是否有可能使用 entailer!
也太 "risky",因为(如文档所述)entailer!
有时可以证明目标变成一个无法证明的目标。试试不带刘海的 entailer
,看看会不会更好看。
其次,TT |-- emp
不成立。 TT
适用于任何堆,emp
只适用于空堆。您可以通过将 pure
函数的后置条件更改为
POST [tint] local(`(eq (Vint (Int.repr 0))) retval) && emp.