budget.dfy

class Budget {
    var days : array<int>
    var weeks : array<int>

    function valid() : bool
        reads this, weeks, days
    {
        days.Length == weeks.Length &&
            (forall i :: 0 <= i < days.Length ==> (weeks[i] == 7 * days[i]))
    }

    method adjustCOLA(cola : int)
        modifies days, weeks

        requires valid()
        ensures valid()
    {
        for i := 0 to days.Length
            invariant valid()   // NOTE: This is required to be explicit
        {
            if (days[i] > 0)
            {
                days[i] := days[i] * cola;
            }

            weeks[i] := 7*days[i]; // This would be synthesized from the data invariant
        }
    }
}