Commit 956ab3f7 authored by charguer's avatar charguer

added_examples

parent 7de702ec
......@@ -19,9 +19,27 @@ Implicit Types n : int.
(* ********************************************************************** *)
(* * Basic functions *)
(* ---------------------------------------------------------------------- *)
(* ** Decrement *)
(** [val_decr] defined in [ExampleBasicNonLifted.v] *)
Lemma Rule_decr : forall (p:loc) (n:int),
Triple (val_decr `p)
PRE (p ~~> n)
POST (fun (r:unit) => p ~~> (n-1)).
Proof using.
xcf. xapps. xapps. xapps. hsimpl~.
Qed.
Hint Extern 1 (Register_Spec val_decr) => Provide Rule_decr.
(* ---------------------------------------------------------------------- *)
(** Swap function *)
(** [val_swap] defined in [ExampleBasicNonLifted.v] *)
Lemma Rule_swap_neq : forall A1 A2 `{EA1:Enc A1} `{EA2:Enc A2} (v:A1) (w:A2) p q,
Triple (val_swap `p `q)
PRE (p ~~> v \* q ~~> w)
......@@ -39,6 +57,41 @@ Proof using.
Qed.
(* ---------------------------------------------------------------------- *)
(** Basic two references *)
Global Opaque Z.mul. (* TODO URGENT *)
Global Opaque Z.add.
(** [val_example_let] defined in [ExampleBasicNonLifted.v] *)
Lemma Rule_val_example_let : forall n,
Triple (val_example_let n)
PRE \[]
POST (fun r => \[r = 2*n]).
Proof using.
xcf. xapps. xapps. xapp. hsimpl. math.
Qed.
(* ---------------------------------------------------------------------- *)
(** Basic let-binding example *)
(** [val_example_ref] defined in [ExampleBasicNonLifted.v] *)
Lemma Rule_val_example_ref : forall n,
Triple (val_example_ref n)
PRE \[]
POST (fun r => \[r = n+1]).
Proof using.
xcf. xapp ;=> i. xapp ;=> r.
xapp~. xapp~. xapps. xapps. xapps. xapps~.
xapps. xapps. xapps.
hsimpl. math.
Qed.
(*
......@@ -102,25 +155,6 @@ Qed.
(***********************************************************************)
(** Basic operations *)
let example_let n =
let a = n+1 in
let b = n-1 in
a + b
let example_incr r =
r := !r + 1
let example_two_ref n =
let i = ref 0 in
let r = ref n in
decr r;
incr i;
r := !i + !r;
!i + !r
(***********************************************************************)
(** For loops *)
......@@ -189,135 +223,6 @@ Qed.
else fib_rec(n-1) + fib_rec(n-2)
(***********************************************************************)
(** Basic operations *)
(*---------------------------------------------------------------------*)
(*----
let example_let n =
let a = n+1 in
let b = n-1 in
a + b
----*)
Lemma example_let_spec : forall n,
app example_let [n]
PRE \[]
POST (fun (v:int) => \[v = 2*n]). (* POST \[= (2 * n)] *)
Proof using.
dup 2.
{ xcf.
xlet. xret. simpl. xpull. intros Ha.
xlet. xret. simpl. xpull. intros Hb.
xret. (*hnf.*) xsimpl. math. }
{ xcf. xret ;=> Ha. xret. intros Hb. xret. xsimpl. math. }
(* use: [xcf], [xret], [xsimpl], [math];
[xlet] is optional; if used then [xpull] is also needed. *)
Qed.
(*---------------------------------------------------------------------*)
(*----
let example_incr r =
r := !r + 1
let example_incr r =
let x0__ := get r in
set r (x0__ + 1)
----*)
Lemma example_incr_spec : forall r n,
app example_incr [r]
PRE (r ~~> n)
POST (fun (_:unit) => (r ~~> (n+1))). (* POST (# r ~~> (n+1)). *)
Proof using.
dup 3.
{ xcf. xlet. xapp. simpl. xpull. intros. subst. xapp. }
{ xcf. xapp. intros. subst. xapp. }
{ xcf. xapps. xapp. }
(* use: [xcf], [xapp];
[xapps] is a shortand for [xapp] followed with [subst] *)
Qed.
(*
Let x0__ := app get [r] in
app set [r (x0__ + 1)]
*)
(* Remark: here are the specifications of get and set from Pervasives_proof.
Lemma get_spec : forall A (v:A) r,
app get [r]
PRE (r ~~> v)
POST (fun x => \[x = v] \* r ~~> v)
Lemma set_spec : forall A (v w:A) r,
app set [r w] (r ~~> v) (# r ~~> w).
*)
(*---------------------------------------------------------------------*)
(*----
let example_two_ref n =
let i = ref 0 in
let r = ref n in
decr r;
incr i;
r := !i + !r;
!i + !r
----*)
Lemma example_two_ref_spec : forall n: int,
(* <EXO> *)
app example_two_ref [n]
PRE \[]
POST (fun x: int => \[ x = n+1 ]).
Proof using.
(*
dup 3.
{xcf. xlet. xapp. simpl. xpull. intros.
xapp.
xapp.
xapp.
xapps. xapps. xapps. xapps. xapps. xret. xsimpl. math.
}
{xcf. xgo. subst. math. }
*)
xcf. xapp. xapp. xapp. xapp. xapps. xapps. xapps. xapps. xapps. xret. xsimpl. math.
Qed.
(*
app example_two_ref [n]
PRE \[]
POST (fun (v:int) => \[v = n+1]).
(* </EXO> *)
Proof using.
(* <EXO> *)
dup.
{ xcf.
xapps.
xapps.
xapps.
xapps.
xapps.
xapps.
xapps.
xapps.
xapps.
xret.
xsimpl.
math. }
{ xcf. xgo~. }
(* </EXO> *)
Qed.
*)
(***********************************************************************)
(** For loops *)
......
......@@ -21,6 +21,10 @@ Implicit Types n : int.
(* ********************************************************************** *)
(* * Basic functions *)
(* ---------------------------------------------------------------------- *)
(** Increment function -- details *)
(* From LambdaStruct
Definition val_incr :=
......@@ -30,9 +34,6 @@ Definition val_incr :=
val_set 'p 'm.
*)
(* ---------------------------------------------------------------------- *)
(** Increment function -- details *)
(** Low-level proof *)
Lemma rule_incr_1 : forall p n,
......@@ -139,6 +140,8 @@ Proof using.
xcf. xapps. xapps. xapps. hsimpl~.
Qed.
Hint Extern 1 (Register_spec val_incr) => Provide rule_incr__7.
(* ---------------------------------------------------------------------- *)
(** Calling incr from a larger context *)
......@@ -177,6 +180,27 @@ Lemma rule_incr_with_frame : forall p n H,
Proof using. intros. xapps. hsimpl~. Qed.
(* ---------------------------------------------------------------------- *)
(** Decrement function -- details *)
Definition val_decr :=
ValFun 'p :=
Let 'n := val_get 'p in
Let 'm := val_sub 'n 1 in
val_set 'p 'm.
Lemma rule_decr : forall p n,
triple (val_decr p)
(p ~~~> n)
(fun r => \[r = val_unit] \* (p ~~~> (n-1))).
Proof using.
xcf. xapps. xapps. xapps. hsimpl~.
Qed.
Hint Extern 1 (Register_spec val_decr) => Provide rule_decr.
(* ---------------------------------------------------------------------- *)
(** Swap function *)
......@@ -225,5 +249,95 @@ Proof using.
Qed.
(* ---------------------------------------------------------------------- *)
(** Basic let-binding example *)
Notation "t1 '+ t2" :=
(val_add t1 t2)
(at level 69) : trm_scope.
Notation "t1 '- t2" :=
(val_sub t1 t2)
(at level 69) : trm_scope.
Notation "'ref t" :=
(val_ref t)
(at level 67) : trm_scope.
Notation "'! t" :=
(val_get t)
(at level 67) : trm_scope.
Notation "t1 ':= t2" :=
(val_set t1 t2)
(at level 67) : trm_scope.
Opaque Z.mul.
Opaque Z.add.
(* URGENT: move *)
Definition val_example_let :=
ValFun 'n :=
Let 'a := 'n '+ 1 in
Let 'b := 'n '- 1 in
'a '+ 'b.
Lemma rule_val_example_let : forall n,
triple (val_example_let n)
\[]
(fun r => \[r = 2*n]).
Proof using.
xcf. xapps. xapps. xapp.
hsimpl. intros. subst. fequals. math.
Qed.
(* ---------------------------------------------------------------------- *)
(** Basic two references *)
(*
let val_example_ref n =
let i = ref 0 in
let r = ref n in
decr r;
incr i;
r := !i + !r;
!i + !r
*)
Definition val_example_ref :=
ValFun 'n :=
Let 'i := 'ref 0 in
Let 'r := 'ref 'n in
val_decr 'r ;;
val_incr 'i ;;
Let 'i1 := '!'i in
Let 'r1 := '!'r in
Let 's := 'i1 '+ 'r1 in
'r ':= 's ;;
Let 'i2 := '!'i in
Let 'r2 := '!'r in
'i2 '+ 'r2.
Lemma rule_val_example_ref : forall n,
triple (val_example_ref n)
\[]
(fun r => \[r = n+1]).
Proof using.
xcf. xapp ;=> i i' Ei. subst.
xapp ;=> r r' Er. subst.
xapp~. xapp~. xapps. xapps. xapps. xapps~.
xapps. xapps. xapps.
hsimpl. intros. subst. fequals. math.
Qed.
......@@ -449,6 +449,7 @@ Hint Extern 1 (Register_Spec (val_prim val_set)) => Provide Rule_set.
Hint Extern 1 (Register_Spec (val_prim val_alloc)) => Provide Rule_alloc.
Hint Extern 1 (Register_Spec (val_prim val_eq)) => Provide Rule_eq.
Hint Extern 1 (Register_Spec (val_prim val_add)) => Provide Rule_add.
Hint Extern 1 (Register_Spec (val_prim val_sub)) => Provide Rule_sub.
Hint Extern 1 (Register_Spec (val_prim val_ptr_add)) => Provide Rule_ptr_add.
......
......@@ -12,7 +12,7 @@ License: MIT.
*)
Set Implicit Arguments.
From TLC Require Export LibString LibCore.
From TLC Require Export LibString LibList LibCore.
From Sep Require Export Fmap TLCbuffer.
Open Scope string_scope.
......
......@@ -719,6 +719,14 @@ Lemma Rule_add : forall n1 n2,
(fun n => \[n = n1 + n2]).
Proof using. intros. unfold Triple, Post. xapplys~ rule_add. Qed.
Lemma Rule_sub : forall n1 n2,
Triple (val_sub n1 n2)
\[]
(fun n => \[n = n1 - n2]).
Proof using. intros. unfold Triple, Post. xapplys~ rule_sub. Qed.
(* TODO URGENT: add other primitives *)
Lemma Rule_ptr_add : forall (l:loc) (n:int),
(l:nat) + n >= 0 ->
Triple (val_ptr_add l n)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment