diff --git a/examples/coincidence_count_list.mlw b/examples/coincidence_count_list.mlw index 29288bc3adcab163502d315bd5149c2e76d93dd0..a21037d1a942dce90251f658c76c1ef395831f4f 100644 --- a/examples/coincidence_count_list.mlw +++ b/examples/coincidence_count_list.mlw @@ -8,7 +8,7 @@ elements that appear in both sequences (in linear time and constant space). - See also coincidence_count for a version using arrays. + See also coincidence_count.mlw for a version using arrays. Authors: Jean-Christophe FilliĆ¢tre (CNRS) *) @@ -19,7 +19,6 @@ module CoincidenceCount use import set.Fset use import list.Elements use list.Mem as L - use import list.Length use import int.Int clone export list.Sorted @@ -29,7 +28,7 @@ module CoincidenceCount requires { sorted a } requires { sorted b } ensures { result == inter (elements a) (elements b) } - variant { length a + length b } + variant { a, b } = match a, b with | Cons ha ta, Cons hb tb -> @@ -44,3 +43,69 @@ module CoincidenceCount end end + +(* the same, with elements of any type *) + +module CoincidenceCountAnyType + + use import list.List + use import set.Fset + use import list.Elements + use list.Mem as L + use import int.Int + + clone import relations.TotalStrictOrder + + clone export list.Sorted + with type t = t, predicate le = rel, goal Transitive.Trans + + let rec coincidence_count (a b: list t) : set t + requires { sorted a } + requires { sorted b } + ensures { result == inter (elements a) (elements b) } + variant { a, b } + = + match a, b with + | Cons ha ta, Cons hb tb -> + if ha = hb then + add ha (coincidence_count ta tb) + else if rel ha hb then + coincidence_count ta b + else + coincidence_count a tb + | _ -> + empty + end + +end + +(* the same, using only lists *) + +module CoincidenceCountList + + use import list.List + use import list.Mem + use import int.Int + + clone export list.Sorted + with type t = int, predicate le = (<), goal Transitive.Trans + + let rec coincidence_count (a b: list int) : list int + requires { sorted a } + requires { sorted b } + ensures { forall x. mem x result <-> mem x a /\ mem x b } + variant { a, b } + = + match a, b with + | Cons ha ta, Cons hb tb -> + if ha = hb then + Cons ha (coincidence_count ta tb) + else if ha < hb then + coincidence_count ta b + else + coincidence_count a tb + | _ -> + Nil + end + +end diff --git a/examples/coincidence_count_list/why3session.xml b/examples/coincidence_count_list/why3session.xml index a06acfb210da6d4a07dc35a195a44fa383b00df5..8c9b3624497fff04b17e6b81d101eacb9bfe59d3 100644 --- a/examples/coincidence_count_list/why3session.xml +++ b/examples/coincidence_count_list/why3session.xml @@ -6,14 +6,14 @@ - - + + - - + + - + @@ -22,11 +22,10 @@ - - + - + @@ -34,11 +33,11 @@ - - + + - + @@ -46,8 +45,8 @@ - - + + @@ -59,5 +58,65 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/coincidence_count_list/why3shapes.gz b/examples/coincidence_count_list/why3shapes.gz index 4d06fd0ceddb57422c6ad372df3936364ca826e6..4d98bc9c3ea34b8a867cb48027db6040572e0fbf 100644 Binary files a/examples/coincidence_count_list/why3shapes.gz and b/examples/coincidence_count_list/why3shapes.gz differ