diff --git a/tests/ggs_db_eqc_test.erl b/tests/ggs_db_eqc_test.erl
new file mode 100644
index 0000000..a29a795
--- /dev/null
+++ b/tests/ggs_db_eqc_test.erl
@@ -0,0 +1,66 @@
+-module(ggs_db_eqc_test).
+
+-include_lib("lib/eqc/include/eqc.hrl").
+
+-compile(export_all).
+
+
+start() ->
+    io:format("prop_set_Item: "),
+    eqc:quickcheck(ggs_db_eqc_test:prop_setItem()),
+    io:format("prop_remove_Item: "),
+    eqc:quickcheck(ggs_db_eqc_test:prop_removeItem()),
+    io:format("prop_clear: "),
+    eqc:quickcheck(ggs_db_eqc_test:prop_clear()),
+    io:format("prop_length: "),
+    eqc:quickcheck(ggs_db_eqc_test:prop_length()),
+    io:format("prop_key: "),
+    eqc:quickcheck(ggs_db_eqc_test:prop_key()).
+
+%% new(length) == old(length) or 
+%% new(length) == old(length) + 1
+prop_setItem() ->
+    ggs_db:init(),           
+    F = (fun(T,N,K,V) -> ggs_db:setItem(T,N,K,V), ggs_db:length(T,N) end),
+    ?FORALL({T,N,K,V},{bitstring(),bitstring(),bitstring(),bitstring()},
+    (ggs_db:length(T,N) + 1 == F(T,N,K,V)) or 
+    (ggs_db:length(T,N) == F(T,N,K,V))).
+
+
+%% new(length) >= 0 and 
+%% old(length) == new(length) or 
+%% old(length) - 1 == new(length) 
+prop_removeItem() ->
+    ggs_db:init(),
+    F = (fun(T,N,K) -> ggs_db:removeItem(T,N,K), ggs_db:length(T,N)  end),
+    G = (fun(A,B) -> ((A == B) or (A == B + 1)) and (B >= 0) end),
+    ?FORALL({T,N,K},{bitstring(),bitstring(),bitstring()},
+    G(ggs_db:length(T,N), F(T,N,K))).
+
+
+%% clear(X) -> (length(X,?) == 0)
+prop_clear() ->
+    ggs_db:init(),
+    F = (fun(T,N) -> ggs_db:clear(T), ggs_db:length(T,N) end),
+    ?FORALL({T,N},{bitstring(),bitstring()},
+    F(T,N) == 0).
+
+%% ? -> length(?,?) >= 0
+prop_length() ->
+    ggs_db:init(),
+    F = fun(T,N,K,V) -> ggs_db:setItem(T,N,K,V), ggs_db:length(T,N) end,
+    G = fun(T,N,K) -> ggs_db:removeItem(T,N,K), ggs_db:length(T,N) end,
+    ?FORALL({{T,N,K,V},{T2,N2,K2}},
+    {{bitstring(),bitstring(),bitstring(),bitstring()},
+    {bitstring(),bitstring(),bitstring()}},
+    (((F(T,N,K,V) >= 0) and (G(T2,N2,K2) >= 0)))).
+
+
+%% key(X,Y,length(X,Y)) -> Exists
+prop_key() ->
+    ggs_db:init(),
+    F = fun(T,N) -> case ggs_db:length(T,N) of 0 -> true; X -> 
+                        case ggs_db:key(T,N,X) of _ -> true end  end end,
+    ?FORALL({T,N},{bitstring(),bitstring()},
+    F(T,N)).
+