VMI Summer Retreat 2019 Master Class on Code Verification

gistfile1.txt

field f: Ref 

define CLOSED(nodes)
    (forall n:Ref :: { n in nodes, n.f } n in nodes && n.f != null ==> n.f in nodes)

define STRUCT(nodes)
    (forall n:Ref :: { n.f } n in nodes ==> acc(n.f)) && 
    !(null in nodes) && 
    CLOSED(nodes)




function root(nodes: Set[Ref], from: Ref): Ref
    requires STRUCT(nodes)
    requires from in nodes
    ensures result in nodes && result.f == null

    // advanced: idempotency
    // ensures root(nodes, result) == result
{
    from.f == null 
        ? from 
        : from.f.f == null? from.f : root(nodes, from.f.f)
}


// Is this sound? 
function sub(nodes: Set[Ref], from: Ref): Set[Ref]
    requires STRUCT(nodes)
    requires from in nodes
    ensures result subset nodes // could this be nodes == result union Set(from)? 
    ensures !(from in result) 
    ensures from.f != null ==> from.f in result
    ensures CLOSED(result)
{
    from.f == null ? Set() : Set(from.f) union sub(nodes, from.f)
}


// Last step: minimization of the specs
method Find(nodes: Set[Ref], x: Ref) returns (y: Ref)
    requires STRUCT(nodes)
    requires x in nodes 
    
    ensures STRUCT(nodes)
    // ensures y in nodes
    
    ensures y == root(nodes, x)
    // ensures x.f != null ==> x != y
    // ensures x != y ==> x.f == y

{
    y := x.f
    if (y != null) {


        var sub_nodes:Set[Ref] := sub(nodes, x)

        label l0
        
        y := Find(sub_nodes, y)

        label l1

        // assert old[l0](x.f) == x.f
        // assume old[l0](x.f) == x.f // implies that x != y
        
        
        

        // assert y == root(nodes, x.f)
        // assert y == root(nodes, x)
        
        x.f := y

        // assert y.f == null
        // assert x.f.f == null
        // assert y == root(nodes, x.f)
        
        
    } else {
        y := x
        // assume false
    }

}


define Blur(g, G) {
    assert g subset g
    assume forall n:Ref :: { root(G, n) } n in g && root(g, n) in g ==> root(g, n) == root(G, n)
}

method Union(nodes: Set[Ref], x: Ref, y: Ref) returns (r: Ref)
    requires STRUCT(nodes)
    requires x in nodes && y in nodes

    ensures STRUCT(nodes)
    // ensures root(nodes, y) == root(nodes, x)
{
    var t: Ref
    var sub_nodes_x: Set[Ref] := sub(nodes, x)
    assert x != null
    t := Find(sub_nodes_x union Set(x), x)

    Blur(sub_nodes_x union Set(x), nodes)
    assert t == root(nodes, x)
    
    var s: Ref
    var sub_nodes_y: Set[Ref] := sub(nodes, y)
    s := Find(sub_nodes_y union Set(y), y)

    Blur(sub_nodes_y union Set(y), nodes)
    assert s == root(nodes, y)

    if (t != s) {
        t.f := s

        assert s == root(nodes, t)
        // idempotency: 
        assume s == root(nodes, x)
    } else {
        assert t == s
        assert t == root(nodes, x)
        assert s == root(nodes, x)
    }

    assert root(nodes, x) == root(nodes, y)
}

method update(s: Ref, t: Ref)
    requires acc(t.f)
    ensures acc(t.f)
    ensures t.f == s
{
    t.f := s
}


// function root(nodes: Set[Ref], from: Ref): Ref
//     requires STRUCT(nodes)
//     requires from in nodes
//     ensures result in nodes && result.f == null
// {
//     from.f == null 
//         ? from 
//         : from.f.f == null? from.f : root(nodes, from.f)
// }

// function root(nodes: Set[Ref], from: Ref): Ref
//     requires STRUCT(nodes)
//     requires from in nodes
//     ensures result in nodes && result.f == null
// {
//     from.f == null ? from : root(nodes, from.f)
// }