Wiki Agenda Contact English version

Hexadecimal encoding of strings

Hexadecimal encoding and decoding of strings.


Auteurs: Cláudio; Lourenço

Catégories: Strings

Outils: 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 ith 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

ObligationsAlt-Ergo 2.3.1CVC4 1.7
VC for hex0.02---
VC for xeh0.02---
decode_unique------
introduce_premises
decode_unique.0------
assert (eq_string s1 s3)
asserted formula0.09---
decode_unique.0.10.01---
VC for encode------
split_vc
loop invariant init0.01---
loop invariant init0.01---
loop invariant init0.05---
loop invariant init0.03---
precondition0.00---
division by zero0.01---
integer overflow0.01---
precondition0.03---
division by zero0.01---
integer overflow------
unfold encoding
integer overflow------
split_vc
integer overflow0.04---
precondition0.06---
integer overflow0.04---
loop variant decrease0.00---
loop invariant preservation0.03---
loop invariant preservation0.07---
loop invariant preservation3.58---
loop invariant preservation1.81---
postcondition------
unfold encoding
VC for encode------
split_vc
VC for encode0.01---
VC for encode---0.19
VC for encode0.04---
VC for decode------
split_vc
division by zero0.03---
integer overflow0.01---
loop invariant init0.05---
loop invariant init0.01---
loop invariant init0.04---
loop invariant init0.04---
precondition0.01---
precondition0.03---
integer overflow0.02---
precondition0.02---
precondition0.14---
integer overflow0.15---
integer overflow0.20---
precondition0.25---
integer overflow0.04---
loop variant decrease0.04---
loop invariant preservation0.10---
loop invariant preservation0.01---
loop invariant preservation0.05---
loop invariant preservation0.54---
postcondition0.15---
VC for decode_encode------
split_vc
precondition0.03---
assertion0.01---