representing strings and associative arrays

Oct 19, 2014 at 3:11 PM
Hello,

This is a beginner's question. How can I represent a string and an (infinite) associative array in Boogie?

Thanks.

Thierry
Oct 19, 2014 at 4:22 PM
Edited Oct 19, 2014 at 10:30 PM
For an infinite associative array you could use a one dimensional map. If your index type is infinite them your map will be as well.
procedure main()
{
    var assocArray:[int]int;
    var otherArray:[int]int;
    var a:int;
    var b:int;
    // Initialise all elements of map to be zero
    assume (forall x:int :: assocArray[x] == 0);
    assume (forall x:int :: otherArray[x] == 0);

    // Boogie might think this assertion can fail
    // due to Maps not having array extensionality
    assert (assocArray == otherArray);

    assocArray[a] := 15;
    otherArray[a] := 15;

    assert (assocArray == otherArray);

    return;
}
Note Boogie by default does treats maps as having extensionality so the assertion can fail in Boogie (if you use /useArrayTheory then as a side effect Maps will be treated as having extensionality).

There is no string data type in Boogie but you can model it using boogie's built in types. Here's an example
// Model a string as a map of integers to 8-bit bitvectors
// where the value corresponds to ascii
type string = [int]bv8;

// Checks string is null terminated
function {:inline true} validStr(s:string) returns(bool)
{
    (exists x:int :: (x >= 0) && (s[x] == 0bv8))
}


procedure {:inline 1} strLen(s:string) returns(length:int)
requires validStr(s);
ensures length >= 0;
{
    length := 0;
    while (s[length] != 0bv8)
    // FIXME: Need loop invariants to prove this correct
    {
        length := length + 1;
    }
}

procedure main()
{
    var myString:string;
    var length:int;

    // Write our string
    myString[0] := 48bv8; // 'H'
    myString[1] := 49bv8; // 'I'

    myString[2] := 0bv8; // '\0' Null terminate

    // Will fail if we forgot to null terminate
    assert validStr(myString);

   call length := strLen(myString);
   assert length == 2;
}
Marked as answer by tsans on 10/20/2014 at 12:11 AM
Oct 20, 2014 at 7:53 AM
This is great. I understand better the philosophy now. Thanks a lot.