2 (** {1 Hexadecimal encoding and decoding of a string}
4 Implementation of functions to encode and decode strings into
7 The length of the encoded string is always twice the length of the
16 use string.StringBuffer
18 (** `valid_hex_char c` is true, if and only if, `c` is a valid
19 hexadecimal character *)
20 predicate valid_hex_char (c: char) =
21 48 <= code c < 58 || 65 <= code c < 71
23 (** `hex i` gives the `i`th hexadecimal value, for `0 <= i < 16` or
25 function hex (i: int) : char =
26 if 0 <= i < 10 then chr (i + 48)
27 else if 10 <= i < 16 then chr (i + 55)
30 let hex (i: int63) : char
31 requires { 0 <= i < 16 }
32 ensures { result = hex i }
33 = if i < 10 then chr (i + 48) else chr (i + 55)
35 (** `xeh c` gives the index of the hexadecimal value `c`, if `c` is a
36 valid hexadecimal value or `-1` otherwise *)
37 function xeh (c: char) : int =
38 if 48 <= code c < 58 then code c - 48
39 else if 65 <= code c < 71 then code c - 55
42 let xeh (c: char) : int63
43 requires { valid_hex_char c }
44 ensures { result = xeh c }
45 = if 48 <= code c < 58 then code c - 48
48 (** checks whether a string contains only valid hexadecimal characters *)
49 predicate valid_hex (s : string) =
50 mod (length s) 2 = 0 &&
51 ( forall i. 0 <= i < length s -> valid_hex_char s[i] )
53 (** `encoding s1 s2` is true, if and only if, `s2` is an encoding of
55 predicate encoding (s1 s2: string) =
56 length s2 = 2 * length s1 &&
57 (forall i. 0 <= i < length s1 ->
58 s1[i] = chr (xeh s2[2 * i] * 16 + xeh s2[2 * i + 1])) &&
61 (** the encoding of a string is unique *)
62 lemma decode_unique: forall s1 s2 s3.
63 encoding s1 s2 /\ encoding s3 s2 -> s1 = s3
65 let encode (s: string) : string
66 ensures { encoding s result }
68 let r = StringBuffer.create (length s) in
69 while i < OCaml.length s do
70 variant { length s - i }
71 invariant { 0 <= i <= length s }
72 invariant { length r = 2 * i }
73 invariant { forall j. 0 <= j < i ->
74 r[2 * j] = hex (div (code s[j]) 16) &&
75 r[2 * j + 1] = hex (mod (code s[j]) 16)
77 invariant { forall j. 0 <= j < 2*i -> valid_hex_char r[j]}
79 StringBuffer.add_char r (hex (v / 16));
80 StringBuffer.add_char r (hex (v % 16));
83 StringBuffer.contents r
85 let decode (s: string) : string
86 requires { valid_hex s }
87 ensures { encoding result s }
89 let r = StringBuffer.create (length s / 2) in
91 variant {length s - i}
92 invariant { mod i 2 = 0 }
93 invariant { 0 <= i <= length s }
94 invariant { length r = div i 2 }
95 invariant { forall j. 0 <= j < div i 2 ->
96 r[j] = chr (xeh s[2 * j] * 16 + xeh s[2 * j + 1]) }
98 let v_ii = xeh s[i + 1] in
99 StringBuffer.add_char r (chr (v_i * 16 + v_ii));
102 StringBuffer.contents r
104 let decode_encode (s: string) : unit
105 = let s1 = encode s in
106 let s2 = decode s1 in