## Hexadecimal encoding of strings

Hexadecimal encoding and decoding of strings.

**Authors:** Cláudio; Lourenço

**Topics:** Strings

**Tools:** Why3

see also the index (by topic, by tool, by reference, by year)

# 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 predicate valid_hex_char (c: char) = 48 <= code c < 58 || 65 <= code c < 71

`valid_hex_char c`

is true, if and only if, `c`

is a valid
hexadecimal character

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]

`hex i`

gives the `i`

th hexadecimal value, for `0 <= i < 16`

or
`0`

otherwise.

let hex (i: int63) : char requires { 0 <= i < 16 } ensures { result = hex i } = if i < 10 then chr (i + 48) else chr (i + 55) 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

`xeh c`

gives the index of the hexadecimal value `c`

, if `c`

is a
valid hexadecimal value or `-1`

otherwise

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 predicate valid_hex (s : string) = mod (length s) 2 = 0 && ( forall i. 0 <= i < length s -> valid_hex_char s[i] )

checks whether a string contains only valid hexadecimal characters

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

`encoding s1 s2`

is true, if and only if, `s2`

is an encoding of
`s1`

lemma decode_unique: forall s1 s2 s3. encoding s1 s2 /\ encoding s3 s2 -> s1 = s3

the encoding of a string is unique

let 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 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 decode_encode (s: string) : unit = let s1 = encode s in let s2 = decode s1 in assert { s = s2 }

download ZIP archive

# Why3 Proof Results for Project "string_hex_encoding"

## Theory "string_hex_encoding.Top": fully verified

Obligations | Alt-Ergo 2.3.1 | CVC4 1.7 | |||

VC for hex | 0.02 | --- | |||

VC for xeh | 0.02 | --- | |||

decode_unique | --- | --- | |||

introduce_premises | |||||

decode_unique.0 | --- | --- | |||

assert (eq_string s1 s3) | |||||

asserted formula | 0.09 | --- | |||

decode_unique.0.1 | 0.01 | --- | |||

VC for encode | --- | --- | |||

split_vc | |||||

loop invariant init | 0.01 | --- | |||

loop invariant init | 0.01 | --- | |||

loop invariant init | 0.05 | --- | |||

loop invariant init | 0.03 | --- | |||

precondition | 0.00 | --- | |||

division by zero | 0.01 | --- | |||

integer overflow | 0.01 | --- | |||

precondition | 0.03 | --- | |||

division by zero | 0.01 | --- | |||

integer overflow | --- | --- | |||

unfold encoding | |||||

integer overflow | --- | --- | |||

split_vc | |||||

integer overflow | 0.04 | --- | |||

precondition | 0.06 | --- | |||

integer overflow | 0.04 | --- | |||

loop variant decrease | 0.00 | --- | |||

loop invariant preservation | 0.03 | --- | |||

loop invariant preservation | 0.07 | --- | |||

loop invariant preservation | 3.58 | --- | |||

loop invariant preservation | 1.81 | --- | |||

postcondition | --- | --- | |||

unfold encoding | |||||

VC for encode | --- | --- | |||

split_vc | |||||

VC for encode | 0.01 | --- | |||

VC for encode | --- | 0.19 | |||

VC for encode | 0.04 | --- | |||

VC for decode | --- | --- | |||

split_vc | |||||

division by zero | 0.03 | --- | |||

integer overflow | 0.01 | --- | |||

loop invariant init | 0.05 | --- | |||

loop invariant init | 0.01 | --- | |||

loop invariant init | 0.04 | --- | |||

loop invariant init | 0.04 | --- | |||

precondition | 0.01 | --- | |||

precondition | 0.03 | --- | |||

integer overflow | 0.02 | --- | |||

precondition | 0.02 | --- | |||

precondition | 0.14 | --- | |||

integer overflow | 0.15 | --- | |||

integer overflow | 0.20 | --- | |||

precondition | 0.25 | --- | |||

integer overflow | 0.04 | --- | |||

loop variant decrease | 0.04 | --- | |||

loop invariant preservation | 0.10 | --- | |||

loop invariant preservation | 0.01 | --- | |||

loop invariant preservation | 0.05 | --- | |||

loop invariant preservation | 0.54 | --- | |||

postcondition | 0.15 | --- | |||

VC for decode_encode | --- | --- | |||

split_vc | |||||

precondition | 0.03 | --- | |||

assertion | 0.01 | --- |