examples/dfa_example.mlw

   1
   2 module DfaExample
   3
   4   (** regular expressions on alphabet {0,1} *)
   5
   6   type char = Zero | One
   7
   8   clone regexp.Regexp with type char = char
   9
  10   (** mutable input stream *)
  11
  12   use option.Option
  13   use seq.Seq
  14
  15   type stream = abstract { mutable state: seq char }
  16
  17   val input: stream
  18
  19   val get () : option char writes {input}
  20     ensures {
  21       if old input.state = empty then
  22         old input.state = input.state = empty /\ result = None
  23       else
  24         input.state = (old input.state)[1..] /\
  25         result = Some ((old input.state)[0]) }
  26
  27   (** 2-state DFA to recognize words ending with a 1, that is (0|1)*1
  28
  29                --------- 1 -------->
  30       +- state 1                    state 2-------+
  31       |    ^   <-------- 0 ---------   ^          |
  32       +-0--/                           \----- 1 --+
  33   *)
  34
  35   constant r0 : regexp = Star (Alt (Char Zero) (Char One))
  36   constant r1 : regexp = Concat r0 (Char One)
  37   constant r2 : regexp = Alt Epsilon r1
  38
  39   lemma empty_notin_r1: not (mem empty r1)
  40
  41   let rec lemma all_in_r0 (w: word)
  42     variant { length w }
  43     ensures { mem w r0 }
  44   = if w = empty then ()
  45     else (
  46       assert { w = (cons w[0] empty) ++ w[1..] };
  47       all_in_r0 w[1..])
  48
  49   lemma words_in_r1_end_with_one:
  50     forall w: word.
  51     mem w r1 <-> exists w': word. w = w' ++ cons One empty
  52
  53   lemma words_in_r1_suffix_in_r1:
  54     forall c c': char. forall w: word.
  55     mem (cons c (cons c' w)) r1 -> mem (cons c' w) r1
  56
  57   lemma zero_w_in_r1: forall w: word. mem w r1 <-> mem (cons Zero w) r1
  58   lemma zero_w_in_r2: forall w: word. mem w r1 <-> mem (cons Zero w) r2
  59   let lemma one_w_in_r1 (w: word)
  60     ensures { mem w r2 <-> mem (cons One w) r1 }
  61   = if length w = 0 then ()
  62     else (
  63       let c = w[0] in
  64       let r = w[1..] in
  65       assert { mem w r2 -> mem w r1 };
  66       assert { mem (cons One (cons c r)) r1 -> mem w r1 }
  67    )
  68
  69   lemma one_w_in_r2:  forall w: word. mem w r2 <-> mem (cons One w) r2
  70
  71   let rec astate1 () : bool
  72     variant { length input.state }
  73     ensures { result <-> input.state = empty /\ mem (old input.state) r1 }
  74   = match get () with
  75     | None      -> false
  76     | Some Zero -> astate1 ()
  77     | Some One  -> astate2 ()
  78     end
  79
  80   with astate2 () : bool
  81     variant { length input.state }
  82     ensures { result <-> input.state = empty /\ mem (old input.state) r2 }
  83   = match get () with
  84     | None      -> true
  85     | Some Zero -> astate1 ()
  86     | Some One  -> astate2 ()
  87     end
  88
  89 end