Commits

yoshihiro503  committed 0b93369

add ynot tutorial

  • Participants
  • Parent commits 614180e

Comments (0)

Files changed (2)

File ynot/tutorial/Counter.v

+Require Import Ynot.
+Open Local Scope hprop_scope.
+
+Module Type COUNTER.
+  Parameter t : Set.
+
+  (* representation predicate *)
+  (* rep c nはcの意味がnですよということをあらわすhprop *)
+  Parameter rep: t -> nat -> hprop.
+
+  (* Cmd pre post はpre状態からpost状態 *)
+  (* __ はemptyなheapの状態 *)
+  (* postコンディションに付随する引数は戻り値を表す *)
+
+  Parameter new : Cmd __ (fun c:t => rep c 0).
+
+  (* [ _ ] はinhabited : Type -> Prop *)
+  (* ~~ はhprop_unpack : forall T:Type, [T] -> (T -> hprop) -> hprop *)
+
+  (* n:[nat] のときnはghost stateと呼ぶ *)
+  (* n ~~ p はspec変数nについて扱うかもしれないhpropの pを表すhprop *)
+
+  Parameter free : forall (c:t) (n: [nat]), Cmd(n ~~ rep c n)
+    (fun _:unit => __).
+
+  (* [n' = n] はhprop(n'=n) でhprop型になる *)
+  (* (p1*p2)はhprop上の掛け算 hprop_sep: hprop->hprop->hprop *)
+
+  Parameter get : forall (c:t) (n: [nat]), Cmd(n ~~ rep c n)
+    (fun n' => n ~~ rep c n * [n' = n]).
+
+  Parameter inc : forall (c:t)(n:[nat]), Cmd (n ~~ rep c n)
+    (fun _:unit => n ~~ rep c (S n)).
+End COUNTER.
+
+Module Counter : COUNTER.
+  Definition t := ptr.
+(*  Definition rep (p: t) (n: nat) := p -> n. *)
+  Definition rep (p : t) (n : nat) := p ~> n.
+  Ltac t := unfold re; sep fail idtac.
+
+  Open Scope stsepi_scope.
+
+  Definition new : Cmd __ (fun c => rep c 0).
+    refine {{ New 0 }} : t.
+  Qed.
+End Counter.

File ynot/tutorial/comp.sh

+coqc -R ~/ynot/src/coq Ynot Counter.v