From 4243f4c8c4dd486e58ffd4d16c48105de34afba1 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Tue, 3 Jun 2014 15:19:51 +0200 Subject: [PATCH] new (simple) example: all_distinct --- examples/all_distinct.mlw | 37 ++++ examples/all_distinct/why3session.xml | 277 ++++++++++++++++++++++++++ 2 files changed, 314 insertions(+) create mode 100644 examples/all_distinct.mlw create mode 100644 examples/all_distinct/why3session.xml diff --git a/examples/all_distinct.mlw b/examples/all_distinct.mlw new file mode 100644 index 000000000..07d1871e5 --- /dev/null +++ b/examples/all_distinct.mlw @@ -0,0 +1,37 @@ + +(** Check an array of integers for duplicate values, + using the fact that values are in interval [0,m-1]. *) + +module AllDistinct + + use import int.Int + use import ref.Ref + use import array.Array + + constant m: int + axiom m_nonneg: 0 <= m + + exception Duplicate + + let all_distinct (a: array int) : bool + requires { forall i: int. 0 <= i < length a -> 0 <= a[i] < m } + ensures { result <-> forall i j: int. 0 <= i < length a -> + 0 <= j < length a -> i <> j -> a[i] <> a[j] } + = + let dejavu = Array.make m False in + try + for k = 0 to Array.length a - 1 do + invariant { forall i j: int. 0 <= i < k -> + 0 <= j < k -> i <> j -> a[i] <> a[j] } + invariant { forall x: int. 0 <= x < m -> + dejavu[x] <-> exists i: int. 0 <= i < k /\ a[i] = x } + let v = a[k] in + if dejavu[v] then raise Duplicate; + dejavu[v] <- True + done; + True + with Duplicate -> + False + end + +end diff --git a/examples/all_distinct/why3session.xml b/examples/all_distinct/why3session.xml new file mode 100644 index 000000000..5a458ea04 --- /dev/null +++ b/examples/all_distinct/why3session.xml @@ -0,0 +1,277 @@ + + + + + + + + + + + -- GitLab