From 2ebdff2625f673c18c79049d91b3da59a5763289 Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Fri, 24 Jun 2022 14:29:44 +0200 Subject: [PATCH 1/2] added first line of gospel in lfu interface --- src/lfu.mli | 52 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/src/lfu.mli b/src/lfu.mli index 8f2daf7..a468057 100644 --- a/src/lfu.mli +++ b/src/lfu.mli @@ -2,20 +2,72 @@ module Make (K : sig type t val equal : t -> t -> bool + (*@ pure*) + val hash : t -> int end) : sig type 'a t type key = K.t + (*@ ephemeral + model cap : int + mutable model assoc : key -> 'a option + mutable model frequency : key -> int + invariant cap > 0 + invariant forall k. assoc k <> None -> frequency > 0 *) + val v : int -> 'a t + (* t = v c + checks c > 0 + ensures t.cap = c + ensures forall k. t.assoc k = None *) + val stats : 'a t -> Stats.t val is_empty : 'a t -> bool + (*@ b = is_empty t + pure + ensures b <-> forall k. t.assoc k = None *) + val capacity : 'a t -> int + (*@ c = capacity t + pure + ensures c = t.cap *) + val size : 'a t -> int + (*@ s = size t + pure *) + val clear : 'a t -> unit + (*@ clear t + modifies t *) + val find : 'a t -> key -> 'a + (*@ v = find t k + ensures t.assoc k = Some v + raises Not_found -> t.assoc k = None + ensures if t.assoc k = Some v then t.frequency k = t.frequency old k + 1 *) + val find_opt : 'a t -> key -> 'a option + (*@ o = find_opt t k + pure + ensures o = t.assoc k + ensures if t.assoc k = Some v then t.frequency k = t.frequency old k + 1 *) + val mem : 'a t -> key -> bool + (*@ b = mem t k + pure + ensures b <-> t.assoc k <> None && t.frequency k = t.frequency old k + 1 *) + val replace : 'a t -> key -> 'a -> unit + (*@ replace t k v + modifies t + ensures t.assoc k = Some v + t.assoc old k <> None -> t.frequency k = t.frequency old k + 1 + t.size < t.cap -> t.assoc old k = None -> + forall k'. t.assoc old k' <> None -> t.assoc k' <> None *) + val remove : 'a t -> key -> unit + (*@ remove t k + modifies t + ensures t.assoc k = None *) end From b70a8957e3d14b47f59afc85783762a45a29f082 Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Mon, 27 Jun 2022 11:01:52 +0200 Subject: [PATCH 2/2] correct lfu contracts, need to comment Format module use in Stats.mli --- src/lfu.mli | 26 ++++++++++++++------------ src/lru.mli | 4 ++-- src/stats.ml | 4 ++-- src/stats.mli | 3 ++- 4 files changed, 20 insertions(+), 17 deletions(-) diff --git a/src/lfu.mli b/src/lfu.mli index a468057..f8d20a6 100644 --- a/src/lfu.mli +++ b/src/lfu.mli @@ -6,15 +6,16 @@ module Make (K : sig val hash : t -> int end) : sig - type 'a t type key = K.t + type 'a t + (*@ ephemeral model cap : int mutable model assoc : key -> 'a option mutable model frequency : key -> int invariant cap > 0 - invariant forall k. assoc k <> None -> frequency > 0 *) + invariant forall k. assoc k <> None <-> frequency k > 0 *) val v : int -> 'a t (* t = v c @@ -35,36 +36,37 @@ end) : sig val size : 'a t -> int (*@ s = size t - pure *) + pure + ensures s <= t.cap *) val clear : 'a t -> unit (*@ clear t - modifies t *) + modifies t + ensures forall k. t.assoc k = None *) val find : 'a t -> key -> 'a (*@ v = find t k - ensures t.assoc k = Some v - raises Not_found -> t.assoc k = None - ensures if t.assoc k = Some v then t.frequency k = t.frequency old k + 1 *) + ensures t.assoc k = Some v -> t.frequency k = t.frequency (old k) + 1 + raises Not_found -> t.assoc k = None *) val find_opt : 'a t -> key -> 'a option (*@ o = find_opt t k pure ensures o = t.assoc k - ensures if t.assoc k = Some v then t.frequency k = t.frequency old k + 1 *) + ensures t.assoc k <> None -> t.frequency k = t.frequency (old k) + 1 *) val mem : 'a t -> key -> bool (*@ b = mem t k pure - ensures b <-> t.assoc k <> None && t.frequency k = t.frequency old k + 1 *) + ensures b <-> t.assoc k <> None && t.frequency k = t.frequency (old k) + 1 *) val replace : 'a t -> key -> 'a -> unit (*@ replace t k v modifies t ensures t.assoc k = Some v - t.assoc old k <> None -> t.frequency k = t.frequency old k + 1 - t.size < t.cap -> t.assoc old k = None -> - forall k'. t.assoc old k' <> None -> t.assoc k' <> None *) + ensures t.assoc (old k) <> None -> t.frequency k = t.frequency (old k) + 1 + ensures t.assoc (old k) = None -> + forall k', v'. t.assoc (old k') = Some v' -> t.assoc k' = Some v' && t.frequency k = 1 *) val remove : 'a t -> key -> unit (*@ remove t k diff --git a/src/lru.mli b/src/lru.mli index a295c39..4badaec 100644 --- a/src/lru.mli +++ b/src/lru.mli @@ -47,10 +47,10 @@ end) : sig raises Not_found -> t.assoc k = None *) val find_opt : 'a t -> key -> 'a option - (*@ o = find_opt t k ensures o = t.assoc k *) - val mem : 'a t -> key -> bool + + val mem : 'a t -> key -> bool (*@ b = mem t k ensures b = true <-> t.assoc k <> None *) diff --git a/src/stats.ml b/src/stats.ml index fd80969..4a94d11 100644 --- a/src/stats.ml +++ b/src/stats.ml @@ -32,7 +32,7 @@ let add new_size t = t.add <- t.add + 1; if t.max_size < new_size then t.max_size <- new_size -let pp ppf t = +(* let pp ppf t = Fmt.pf ppf {|miss : %d hit : %d @@ -42,4 +42,4 @@ let pp ppf t = remove : %d clear : %d maximal size : %d|} - t.miss t.hit t.add t.replace t.discard t.remove t.clear t.max_size + t.miss t.hit t.add t.replace t.discard t.remove t.clear t.max_size *) diff --git a/src/stats.mli b/src/stats.mli index d3ac3ad..8251a05 100644 --- a/src/stats.mli +++ b/src/stats.mli @@ -64,4 +64,5 @@ val add : int -> t -> unit ensures t.max_size >= old t.max_size *) -val pp : Format.formatter -> t -> unit +(* val pp : Format.formatter -> t -> unit *) +