dfa_example.mlw 2.55 KB
Newer Older
1 2 3 4 5 6 7

module DfaExample

  (** regular expressions on alphabet {0,1} *)

  type char = Zero | One

8
  clone regexp.Regexp with type char = char
9 10 11

  (** mutable input stream *)

12
  use option.Option
13

14
  type stream = abstract { mutable state: list char }
15 16 17

  val input: stream

18
  use list.Length
MARCHE Claude's avatar
MARCHE Claude committed
19

20 21 22 23 24 25 26 27 28 29 30 31 32
  val get () : option char writes {input}
    ensures { match old input.state with
    | Cons c l -> input.state = l /\ result = Some c
    | Nil -> old input.state = input.state = Nil /\ result = None end }

  (** 2-state DFA to recognize words ending with a 1, that is (0|1)*1

               --------- 1 -------->
      +- state 1                    state 2-------+
      |    ^   <-------- 0 ---------   ^          |
      +-0--/                           \----- 1 --+
  *)

MARCHE Claude's avatar
MARCHE Claude committed
33 34
  constant r0 : regexp = Star (Alt (Char Zero) (Char One))
  constant r1 : regexp = Concat r0 (Char One)
35 36 37 38
  constant r2 : regexp = Alt Epsilon r1

  lemma nil_notin_r1: not (mem Nil r1)

MARCHE Claude's avatar
MARCHE Claude committed
39 40 41 42 43 44 45 46 47 48
  let rec lemma all_in_r0 (w: list char)
    variant { w }
    ensures { mem w r0 }
  = match w with
    | Nil -> ()
    | Cons c r ->
      assert { w = (Cons c Nil) ++ r } ;
      all_in_r0 r
    end

MARCHE Claude's avatar
MARCHE Claude committed
49
  lemma words_in_r1_end_with_one:
50 51 52
    forall w: list char.
    mem w r1 <-> exists w': list char. w = w' ++ Cons One Nil

MARCHE Claude's avatar
MARCHE Claude committed
53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
  let lemma words_in_r1_suffix_in_r1 (c c':char) (w: list char)
    requires { mem (Cons c (Cons c' w)) r1 }
    ensures  { mem (Cons c' w) r1 }
  = assert { exists w'. (Cons c (Cons c' w))  = w' ++ Cons One Nil }

  let lemma zero_w_in_r1 (w: list char)
    ensures { mem w r1 <-> mem (Cons Zero w) r1 }
  = assert { mem (Cons Zero w) r1 ->
             exists w'. (Cons Zero w)  = w' ++ Cons One Nil }

  let lemma one_w_in_r1 (w: list char)
    ensures { mem w r2 <-> mem (Cons One w) r1 }
  = match w with
    | Nil -> ()
    | Cons c r ->
      assert { mem w r2 -> mem w r1 };
      assert { mem (Cons One (Cons c r)) r1 -> mem w r1 }
    end
71 72 73 74 75

  lemma zero_w_in_r2: forall w: list char. mem w r1 <-> mem (Cons Zero w) r2
  lemma one_w_in_r2: forall w: list char. mem w r2 <-> mem (Cons One w) r2

  let rec astate1 () : bool
MARCHE Claude's avatar
MARCHE Claude committed
76
    variant { length input.state }
77 78 79 80 81 82 83 84 85
    ensures { result = True <-> input.state = Nil /\ mem (old input.state) r1 }
    =
    match get () with
    | None      -> False
    | Some Zero -> astate1 ()
    | Some One  -> astate2 ()
    end

  with astate2 () : bool
MARCHE Claude's avatar
MARCHE Claude committed
86
    variant { length input.state }
87 88 89 90 91 92 93 94 95
    ensures { result = True <-> input.state = Nil /\ mem (old input.state) r2 }
    =
    match get () with
    | None      -> True
    | Some Zero -> astate1 ()
    | Some One  -> astate2 ()
    end

end