NamArray.dfy

// NamArray is basically the same as an array, but way better because it has 4 improvements
//  1- Cannot remove elements from the array. Removing stuff is for cowards
//  2- Can only append to the end of the array. That way it's auto sorted in chronological order
//  3- Is bounded
//  4- For every 3 items added to the array, another "Nam" gets added to the NamString.

// When writing Valid(), constructor(), functions, and methods, a lot of the fundamentals are copied directly from the final 3 slides of week 9
class NamArray<T(0)> {
    // Abstract state - What the user sees
    ghost var s: seq<T> // Remember that in Dafny, 'seq' is ordered
    ghost var NamString: string // Dafny type "string" is a wrapper for seq<char>
    ghost const max: nat // Type 'nat' is always >0
    ghost var Repr: set<object> // Complicated memory aliasing stuff

    // Concrete state - What the class is actually made of
    var a: array<T> // What 's' actually is. 's' and 'a' are going to be practically identical
    var ns: array<char> // What 'NamString' actually is. 'NamString' and 'ns' are going to be practically identical
    var count: nat // The amount of items in 's' and 'NamString'.

    // Valid() is basically an invariant for an entire class
    ghost predicate Valid()
        // Copied directly from end of week 9 lecture slides
        reads this, Repr
        ensures Valid() ==> this in Repr

        // Relationships inside the abstract state (if any)
        ensures Valid() ==> |s| <= max // 's' is bounded correctly
        ensures Valid() ==> |NamString| <= max // 'NamString' is bounded correctly
        ensures Valid() ==> (forall c :: 0 <= c < |NamString| ==>
            if c % 3 == 0 then      NamString[c] == 'N'
            else if c % 3 == 1 then NamString[c] == 'a'
            else                    NamString[c] == 'm'
        ) // 'NamString' is "Nam" repeated
    {
        // Copied directly from end of week 9 lecture slides
        // Be aware that the order of statements in here matters - stuff with Repr has to be first, etc
        this in Repr &&
        a in Repr &&
        ns in Repr &&
        a != ns && // 'a' is of generic type 'T', which means it's possible for
                    // 'a' and 'ns' to be of the same type, so they must be declared to be disjoint in memory

        // Relationships between the abstract and concrete state (if any)
        |s| == |NamString| == count <= a.Length == ns.Length == max && // Bounds and lengths

        s == a[..count] && // What 's' actually is - the first 'count' elements in 'a'

        NamString == ns[..count] && // What 'ns' actually is - the first 'count' elements in 'NamString'
                // Remember that with [i..j], 'i' is inclusive and 'j' is exclusive


        // Relationships inside the concrete state (if any)
        forall c :: 0 <= c < count ==> (
            if c % 3 == 0 then      ns[c] == 'N'
            else if c % 3 == 1 then ns[c] == 'a'
            else                    ns[c] == 'm'
        ) // NamString is "Nam" repeated
    }

    // Initializes NamArray
    constructor(max: nat)
        ensures Valid() && fresh(Repr) // Copied directly from end of week 9 lecture slides

        ensures s == [] // 's' is initialized to be empty
        ensures NamString == []  // 'NamString' is initialized to be empty
        ensures this.max == max // this.max is initialized to be the supplied 'max'
    {
        // Concrete state
        a := new T[max]; // Initialize 'a' to be array of size 'max'
        ns := new char[max]; // Initialize 'ns' to be char array of size 'max'
        count := 0; // No elements, so count = 0

        // Abstract state
        s := [];
        NamString := "";
        this.max := max;
        Repr := {this, a, ns};
        // We don't need "new;" because we don't have a composite object
    }

    function Size(): nat
        // Copied directly from end of week 9 lecture slides
        requires Valid()
        reads Repr
        ensures Size() == |s| // |s| is len(s) - sequence notation is the final lecture slide of week7
    {
        count
    }

    function GetS(): seq<T>
        // Copied directly from end of week 9 lecture slides
        requires Valid()
        reads Repr
        ensures GetS() == s
    {
        a[..count]
    }

    function GetNamString(): string
        // Copied directly from end of week 9 lecture slides
        requires Valid()
        reads Repr
        ensures GetNamString() == NamString
    {
        ns[..count]
    }

    method Append(x: T)
        // Copied directly from end of week 9 lecture slides
        requires Valid()
        modifies Repr
        ensures Valid() && fresh(Repr - old(Repr))

        requires |s| < max // Can't append when the maximum has been reached
        ensures s == old(s) + [x] // 'Append()' adds to the end of 's'
        ensures (
            if |NamString| % 3 == 0 then        NamString == old(NamString) + ['m']
            else if |NamString| % 3 == 1 then   NamString == old(NamString) + ['N']
            else                                NamString == old(NamString) + ['a']
        ) // 'NamString' is "Nam" repeated
    {
        a[count] := x;

        var char_to_add;
        if (count % 3 == 0) {
            char_to_add := 'N';
        } else if (count % 3 == 1) {
            char_to_add := 'a';
        } else {
            char_to_add := 'm';
        }
        ns[count] := char_to_add;

        count := count + 1;

        s := old(s) + [x];
        NamString := old(NamString) + [char_to_add];
        // Note that code is needed for both the abstract and concrete state
    }
}

method testNamArray()
{
    var na := new NamArray<int>(10);
    assert na.Size() == 0;
    assert na.s == [];
    assert na.NamString == "";

    na.Append(1);
    na.Append(2);
    assert na.GetNamString() == "Na";
    na.Append(3);
    assert na.GetNamString() == "Nam";
    na.Append(4);
    na.Append(5);
    assert na.GetNamString() == "NamNa";
    na.Append(6);
    
    assert na.Size() == 6;
    assert na.s == [1,2,3,4,5,6];
    assert na.NamString == "NamNam";
    var arr := na.GetS();
    var nam := na.GetNamString();
    assert arr == [1,2,3,4,5,6];
    assert nam == "NamNam";
    assert arr == na.s;
    assert nam == na.NamString;

    na.Append(7);
    na.Append(8);
    na.Append(9);
    na.Append(10);
    assert na.GetNamString() == "NamNamNamN";
}