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