Documentation/tutorial for ortac-stm plugin

dune-project

@@ -1,5 +1,7 @@
-(lang dune 3.0)
+(lang dune 3.8)
 (using dune_site 0.1)
+(using mdx 0.4)
+
 (name ortac)
 
 (package

ortac-core.opam

@@ -29,7 +29,7 @@ build: [
 
 depends: [
   "ocaml" {>= "4.11.0"}
-  "dune" {>= "3.0"}
+  "dune" {>= "3.8"}
   "dune-site"
   "cmdliner" {>= "1.1.0"}
   "fmt"

ortac-monolith.opam

@@ -24,7 +24,7 @@ build: [
 
 depends: [
   "ocaml" {>= "4.11.0"}
-  "dune" {>= "3.0"}
+  "dune" {>= "3.8"}
   "cmdliner" {>= "1.1.0"}
   "fmt"
   "ppxlib" {>= "0.26.0"}

ortac-qcheck-stm.opam

@@ -27,10 +27,11 @@ build: [
 
 depends: [
   "ocaml" {>= "4.11.0"}
-  "dune" {>= "3.0"}
+  "dune" {>= "3.8"}
   "cmdliner" {>= "1.1.0"}
   "fmt"
   "ppxlib" {>= "0.26.0"}
+  "mdx" {with-test}
   "gospel" {>= "0.2.0"}
   "qcheck-core" {with-test}
   "qcheck-stm" {with-test}

ortac-runtime-monolith.opam

@@ -24,7 +24,7 @@ build: [
 
 depends: [
   "ocaml" {>= "4.11.0"}
-  "dune" {>= "3.0"}
+  "dune" {>= "3.8"}
   "monolith" {>= "20201026"}
   "pprint"
   "fmt" {>= "0.9.0"}

ortac-runtime.opam

@@ -12,7 +12,7 @@ doc: "https://pascutto.github.io/ortac/"
 bug-reports: "https://github.com/ocaml-gospel/ortac/issues"
 depends: [
   "ocaml" {>= "4.11.0"}
-  "dune" {>= "3.0"}
+  "dune" {>= "3.8"}
   "fmt"
   "zarith"
   "monolith" {with-test}

ortac-wrapper.opam

@@ -28,7 +28,7 @@ build: [
 
 depends: [
   "ocaml" {>= "4.11.0"}
-  "dune" {>= "3.0"}
+  "dune" {>= "3.8"}
   "dune-site"
   "cmdliner" {>= "1.1.0"}
   "fmt"

plugins/qcheck-stm/doc/dune

@@ -0,0 +1,20 @@
+(mdx
+ (package ortac-qcheck-stm)
+ (deps
+  (package ortac-core)
+  (package ortac-qcheck-stm)))
+
+(documentation
+ (package ortac-qcheck-stm)
+ (mld_files index))
+
+(rule
+ (alias runtest)
+ (package ortac-qcheck-stm)
+ (deps
+  (:examples
+   (glob_files *.mli))
+  (package gospel))
+ (action
+  (ignore-outputs
+   (run gospel check %{examples}))))

plugins/qcheck-stm/doc/example.mli

@@ -0,0 +1,36 @@
+(* $MDX part-begin=type-decl *)
+
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+
+(* $MDX part-end *)
+
+(* $MDX part-begin=make *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+
+(* $MDX part-end *)
+
+(* $MDX part-begin=set *)
+
+val set : 'a t -> int -> 'a -> unit
+(*@ set t i a
+    checks 0 <= i < t.size
+    modifies t.contents
+    ensures t.contents = List.mapi (fun j x -> if j = (i : integer) then a else x) (old t.contents) *)
+
+(* $MDX part-end *)
+
+(* $MDX part-begin=get *)
+
+val get : 'a t -> int -> 'a
+(*@ a = get t i
+    checks 0 <= i < t.size
+    ensures a = List.nth t.contents i *)
+
+(* $MDX part-end *)

plugins/qcheck-stm/doc/example_for_all.mli

@@ -0,0 +1,17 @@
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+
+(* $MDX part-begin=fun-decl *)
+
+val for_all : 'a t -> bool
+(*@ b = for_all t
+    ensures b = List.for_all (fun x -> x = x) t.contents *)
+
+(* $MDX part-end *)

plugins/qcheck-stm/doc/example_ghost.mli

@@ -0,0 +1,16 @@
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+
+(* $MDX part-begin=fun-decl *)
+
+val ghost_arg : char -> 'a t -> bool
+(*@ b = ghost_arg [ i : integer] c t *)
+
+(* $MDX part-end *)

plugins/qcheck-stm/doc/example_ill_formed_quantification.mli

@@ -0,0 +1,17 @@
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+
+(* $MDX part-begin=fun-decl *)
+
+val unsupported_quantification : 'a t -> bool
+(*@ b = unsupported_quantification t
+    ensures b = forall a. List.mem a t.contents -> a = a *)
+
+(* $MDX part-end *)

plugins/qcheck-stm/doc/example_incompatible_type.mli

@@ -0,0 +1,16 @@
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+
+(* $MDX part-begin=fun-decl *)
+
+val incompatible_type : char -> string t -> bool
+(*@ b = incompatible_type c t *)
+
+(* $MDX part-end *)

plugins/qcheck-stm/doc/example_limitations.mli

@@ -0,0 +1,31 @@
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+
+(* $MDX part-begin=fun-decl *)
+
+val f : int -> int -> bool
+(*@ b = f x y *)
+
+val compare : 'a t -> 'a t -> bool
+(*@ b = compare t1 t2 *)
+
+val of_list : 'a list -> 'a t
+(*@ t = of_list xs *)
+
+val g : int * int -> 'a t -> bool
+(*@ b = g x t *)
+
+val h : 'a t -> 'a * 'a
+(*@ (l, r) = h t *)
+
+val for_all : ('a -> bool) -> 'a t -> bool
+(*@ b = for_all p t *)
+
+(* $MDX part-end *)

plugins/qcheck-stm/doc/example_next_state.mli

@@ -0,0 +1,18 @@
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+
+(* $MDX part-begin=fun-decl *)
+
+val ensures_not_found_for_next_state : 'a t -> unit
+(*@ ensures_not_found_for_next_state t
+    modifies t.contents
+    ensures List.length t.contents = List.length (old t.contents) *)
+
+(* $MDX part-end *)

plugins/qcheck-stm/doc/example_unknown_type.mli

@@ -0,0 +1,18 @@
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+
+type new_type
+
+(* $MDX part-begin=fun-decl *)
+
+val type_not_supported : new_type -> 'a t -> new_type
+(*@ y = type_not_supported x t *)
+
+(* $MDX part-end *)