method Add(s1: string, s2: string) returns (res: string)

  requires ValidBitString(s1) && ValidBitString(s2)

  ensures ValidBitString(res)

  ensures Str2Int(res) == Str2Int(s1) + Str2Int(s2)

{

  var i := Str2Int(s1);

  var j := Str2Int(s2);

  var k := i + j;

  res := Int2Str(k); 

}

​

function Int2Str(n: nat): string 

    requires n >= 0

    ensures ValidBitString(Int2Str(n))

    ensures Str2Int(Int2Str(n)) == n 

{   

    if n == 0 then "0"

    else if n == 1 then "1"

    else if n % 2 == 0 then Int2Str(n / 2) + "0"

    else Int2Str(n / 2) + "1"

}

​

function Str2Int(s: string): nat 

    requires ValidBitString(s)

{

    if s == "0" then 0

    else if s == "1" then 1

    else if s[|s|-1] == '0' then 2 * Str2Int(s[..|s|-1])

    else 2 * Str2Int(s[..|s|-1]) + 1

}

predicate ValidBitString(s: string) {

    |s| >= 1 && 

    (forall i | 0 <= i < |s| :: s[i] == '0' || s[i] == '1') &&

    (if |s| > 1 then s[0] == '1' else true)

}