Forking Stack Datastructure

[alcides]

This is the data structure that works as a stack, but allows for forking for branching (for if statements).

Sketch:

fun(int a) {
    int b = 0;
    if (a  > 0) {
        a = -1; # a_1 == -1

        @Refinement("c > 0") int c = 1;

        if (a > b) {
            b = a;
        } else {
            a = b;
        }

        c = c + 1;      #  c4 == c_1 + 1 => c4 > 0

    } else {
        a = -3; # a_2 == -3
        a = a + 1 # a_3
    }

    # a_6 = ite(a_0 > 0, a_1, a_3)

    assert(a > b)
}

[b0, FORK, FORK, a6, b6]
            -> c1false, a4, a5, 
     -> c1true, a1, FORK, FORK, b3, a3]
                             -> c2false, a2
                        -> [ MARK, c2true, b1 ]

Elements of the Stack can be either: GlobalBinding or LocalBinding

[alcides]

Note: The solution for this is the MERGE operation defined in the formal type checking draft.