examples/residual.mlw

   1
   2 (** {1 Decision of regular expression membership} *)
   3
   4 (** Decision algorithm based on residuals *)
   5
   6 module Residual
   7
   8   type char
   9
  10   val predicate eq (x y : char)
  11     ensures { result <-> x = y }
  12
  13   clone regexp.Regexp with type char = char
  14
  15   use seq.Seq
  16   use int.Int
  17
  18   let rec accepts_epsilon (r: regexp) : bool
  19     variant { r }
  20     ensures { result <-> mem empty r }
  21   = match r with
  22     | Empty -> false
  23     | Epsilon -> true
  24     | Char _ -> false
  25     | Alt r1 r2 -> accepts_epsilon r1 || accepts_epsilon r2
  26     | Concat r1 r2 -> accepts_epsilon r1 && accepts_epsilon r2
  27     | Star _ -> true
  28     end
  29
  30   lemma inversion_mem_star_gen :
  31     forall c w r w' r'.
  32       w' = cons c w /\ r' = Star r ->
  33       mem w' r' ->
  34       exists w1 w2. w = w1 ++ w2 /\ mem (cons c w1) r /\ mem w2 r'
  35
  36   lemma inversion_mem_star :
  37     forall c w r. mem (cons c w) (Star r) ->
  38       exists w1 w2. w = w1 ++ w2 /\ mem (cons c w1) r /\ mem w2 (Star r)
  39
  40   (** `residual r c` denotes the set of words `w` such that `mem c.w r` *)
  41   let rec residual (r: regexp) (c: char) : regexp
  42     variant { r }
  43     ensures { forall w. mem w result <-> mem (cons c w) r }
  44   = match r with
  45     | Empty -> Empty
  46     | Epsilon -> Empty
  47     | Char c' -> if eq c c' then Epsilon else Empty
  48     | Alt r1 r2 -> alt (residual r1 c) (residual r2 c)
  49     | Concat r1 r2 ->
  50         let r1' = residual r1 c in
  51         let r2' = residual r2 c in
  52         if accepts_epsilon r1 then (
  53           assert {
  54             forall w: word.
  55               mem w (Alt (Concat r1' r2) r2') <->
  56               mem (cons c w) r
  57           };
  58           alt (concat r1' r2) r2')
  59         else concat r1' r2
  60     | Star r1 -> concat (residual r1 c) r
  61     end
  62
  63   let decide_mem (w: word) (r: regexp) : bool
  64     ensures { result <-> mem w r }
  65   = let ref r' = r in
  66     for i = 0 to length w - 1 do
  67       invariant { mem w[i..] r' <-> mem w r }
  68       r' <- residual r' w[i]
  69     done;
  70     accepts_epsilon r'
  71
  72 end
  73
  74 module ResidualOCaml
  75
  76   use int.Int
  77   use mach.int.Int63
  78   use seq.Seq
  79   clone export Residual
  80   import Regexp
  81
  82   type ostring = abstract {
  83      str: seq char
  84   }
  85   meta coercion function str
  86
  87   val ([]) (s: ostring) (i: int63) : char
  88     requires { 0 <= i < length s }
  89     ensures  { result = get s i }
  90
  91   val partial length (s: ostring) : int63
  92     ensures { result = length s >= 0 }
  93
  94   let partial decide (w: ostring) (r: regexp) : bool
  95     ensures { result <-> mem w r }
  96   = let ref r' = r in
  97     for i = 0 to length w - 1 do
  98       invariant { mem w[i..] r' <-> mem w r }
  99       r' <- residual r' w[i]
 100     done;
 101     accepts_epsilon r'
 102
 103 end