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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
|
(** {1 Hexadecimal encoding and decoding of a string}
Implementation of functions to encode and decode strings into
hexadecimal.
The length of the encoded string is always twice the length of the
input string.
*)
use mach.int.Int
use mach.int.Int63
use string.String
use string.Char
use string.OCaml
use string.StringBuffer
(** `valid_hex_char c` is true, if and only if, `c` is a valid
hexadecimal character *)
predicate valid_hex_char (c: char) =
48 <= code c < 58 || 65 <= code c < 71
(** `hex i` gives the `i`th hexadecimal value, for `0 <= i < 16` or
`0` otherwise. *)
function hex (i: int) : char =
if 0 <= i < 10 then chr (i + 48)
else if 10 <= i < 16 then chr (i + 55)
else "\000"[0]
let hex (i: int63) : char
requires { 0 <= i < 16 }
ensures { result = hex i }
= if i < 10 then chr (i + 48) else chr (i + 55)
(** `xeh c` gives the index of the hexadecimal value `c`, if `c` is a
valid hexadecimal value or `-1` otherwise *)
function xeh (c: char) : int =
if 48 <= code c < 58 then code c - 48
else if 65 <= code c < 71 then code c - 55
else -1
let xeh (c: char) : int63
requires { valid_hex_char c }
ensures { result = xeh c }
= if 48 <= code c < 58 then code c - 48
else code c - 55
(** checks whether a string contains only valid hexadecimal characters *)
predicate valid_hex (s : string) =
mod (length s) 2 = 0 &&
( forall i. 0 <= i < length s -> valid_hex_char s[i] )
(** `encoding s1 s2` is true, if and only if, `s2` is an encoding of
`s1` *)
predicate encoding (s1 s2: string) =
length s2 = 2 * length s1 &&
(forall i. 0 <= i < length s1 ->
s1[i] = chr (xeh s2[2 * i] * 16 + xeh s2[2 * i + 1])) &&
valid_hex s2
(** the encoding of a string is unique *)
lemma decode_unique: forall s1 s2 s3.
encoding s1 s2 /\ encoding s3 s2 -> s1 = s3
let partial encode (s: string) : string
ensures { encoding s result }
= let ref i = 0 in
let r = StringBuffer.create (length s) in
while i < OCaml.length s do
variant { length s - i }
invariant { 0 <= i <= length s }
invariant { length r = 2 * i }
invariant { forall j. 0 <= j < i ->
r[2 * j] = hex (div (code s[j]) 16) &&
r[2 * j + 1] = hex (mod (code s[j]) 16)
}
invariant { forall j. 0 <= j < 2*i -> valid_hex_char r[j]}
let v = code s[i] in
StringBuffer.add_char r (hex (v / 16));
StringBuffer.add_char r (hex (v % 16));
i <- i + 1
done;
StringBuffer.contents r
let partial decode (s: string) : string
requires { valid_hex s }
ensures { encoding result s }
= let ref i = 0 in
let r = StringBuffer.create (length s / 2) in
while i < length s do
variant {length s - i}
invariant { mod i 2 = 0 }
invariant { 0 <= i <= length s }
invariant { length r = div i 2 }
invariant { forall j. 0 <= j < div i 2 ->
r[j] = chr (xeh s[2 * j] * 16 + xeh s[2 * j + 1]) }
let v_i = xeh s[i] in
let v_ii = xeh s[i + 1] in
StringBuffer.add_char r (chr (v_i * 16 + v_ii));
i <- i + 2
done;
StringBuffer.contents r
let partial decode_encode (s: string) : unit
= let s1 = encode s in
let s2 = decode s1 in
assert { s = s2 }
|
