examples/subsequence.mlw

   1
   2 (** {1 Subsequences}
   3
   4   A subsequence is a sequence that can be derived from another
   5   sequence by deleting some or no elements without changing the order
   6   of the remaining elements (Wikipedia).
   7
   8   Checking whether a word is a subsequence of another word can be done in
   9   linear time (in the length of the second word) and is a nice example of
  10   an optimal greedy algorithm.
  11
  12   Author: Jean-Christophe Filliâtre (CNRS)
  13
  14 *)
  15
  16 use int.Int
  17 use map.Map
  18 use seq.Seq
  19
  20 type char
  21 type word = seq char
  22
  23 predicate subsequence (v u: word) (f: int -> int) =
  24   (* f maps v's characters to u's characters *)
  25   (forall i. 0 <= i < length v -> 0 <= f i < length u /\ v[i] = u[f i]) /\
  26   (* in a strictly increasing way *)
  27   (forall i j. 0 <= i < j < length v -> f i < f j)
  28
  29 val eq (x y: char) : bool ensures { result <-> x = y }
  30
  31 let is_subsequence (v u: word) : bool
  32   ensures { result <-> exists f. subsequence v u f }
  33 = let rec aux (i j: int) (ghost f: int -> int) : bool
  34     requires { 0 <= i <= length v }
  35     requires { 0 <= j <= length u }
  36     requires { subsequence v[0..i] u[0..j] f }
  37     requires { forall f. subsequence v u f -> i < length v -> f i >= j }
  38     variant  { length u - j }
  39     ensures  { result <-> exists f. subsequence v u f }
  40   = i = length v ||
  41     j < length u && if eq v[i] u[j] then aux (i+1) (j+1) (Map.set f i j)
  42                                     else aux     i (j+1) f
  43   in
  44   aux 0 0 (fun i -> i)
  45