1 files changed, 31 insertions, 0 deletions
diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml
new file mode 100644
index 0000000..fb01ac6
--- /dev/null
+++ b/abstract/value_domain.ml
@@ -0,0 +1,31 @@
+module type VALUE_DOMAIN = sig
+    type t
+
+    (* constructors *)
+    val top     : t
+    val bottom  : t
+    val const   : int -> t
+    val rand    : int -> int -> t
+
+    (* order *)
+    val subset  : t -> t -> bool
+
+    (* set-theoretic operations *)
+    val join    : t -> t -> t   (* union *)
+    val meet    : t -> t -> t   (* intersection *)
+    val widen   : t -> t -> t
+
+    (* arithmetic operations *)
+    val neg     : t -> t
+    val add     : t -> t -> t
+    val sub     : t -> t -> t
+    val mul     : t -> t -> t
+    val div     : t -> t -> t
+    val rem     : t -> t -> t
+
+    (* boolean test *)
+    val leq     : t -> t -> t * t   (* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *)
+
+    (* pretty-printing *)
+    val to_string : t -> string
+end