mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
96 lines
2.5 KiB
Plaintext
96 lines
2.5 KiB
Plaintext
|
|
module DfaExample
|
|
|
|
(** regular expressions on alphabet {0,1} *)
|
|
|
|
type char = Zero | One
|
|
|
|
clone regexp.Regexp with type char = char
|
|
|
|
(** mutable input stream *)
|
|
|
|
use option.Option
|
|
|
|
type stream = abstract { mutable state: list char }
|
|
|
|
val input: stream
|
|
|
|
use list.Length
|
|
|
|
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 --+
|
|
*)
|
|
|
|
constant r0 : regexp = Star (Alt (Char Zero) (Char One))
|
|
constant r1 : regexp = Concat r0 (Char One)
|
|
constant r2 : regexp = Alt Epsilon r1
|
|
|
|
lemma nil_notin_r1: not (mem Nil r1)
|
|
|
|
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
|
|
|
|
lemma words_in_r1_end_with_one:
|
|
forall w: list char.
|
|
mem w r1 <-> exists w': list char. w = w' ++ Cons One Nil
|
|
|
|
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
|
|
|
|
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
|
|
variant { length input.state }
|
|
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
|
|
variant { length input.state }
|
|
ensures { result = True <-> input.state = Nil /\ mem (old input.state) r2 }
|
|
=
|
|
match get () with
|
|
| None -> True
|
|
| Some Zero -> astate1 ()
|
|
| Some One -> astate2 ()
|
|
end
|
|
|
|
end
|