method part2BU<E>( S : set<E> ) returns (R : set< (set<E>, set<E>) > )
// ensures R is the set of all pairs of sets (T,U)
//           such that (T,U) is a partition of S
decreases |S|
{
    if S == {} {
        R := {({}, {})} ; }
    else {
        R := {} ;
        var x :| x in S ;
        var P := part2BU( S-{x}) ;
        while( P != {} )
            decreases |P|
        {
            assert |P| > 0 ;
            var pair :| pair in P ;
            var (T,U) := pair ;
            R := R + {(T+{x}, U), (T, U+{x})} ;
            P := P - { pair } ; } }
}

method part2TD<E>( S : set<E> ) returns (R : set< (set<E>, set<E>) > )
// ensures R is the set of all pairs of sets (T,U)
//           such that (T,U) is a partition of S
{
    R := part2TD_aux( S, {}, {} ) ;
}

method part2TD_aux<E>( S : set<E>, T_in : set<E>, U_in : set<E> )
returns (R : set< (set<E>, set<E>) > )
//     ensures R is the set of all pairs of sets (T,U)
//                such that (T,U) is a partition of S union T_in union U_in
//                          and T is a superset of T_in
//                          and U is a superset of U_in
decreases |S|
{
    if S == {} {
        R := {( T_in, U_in)} ; }
    else {
        var x :| x in S ;
        var Left := part2TD_aux( S-{x}, T_in + {x}, U_in ) ;
        var Right := part2TD_aux( S-{x}, T_in, U_in + {x} ) ;
        R := Left + Right ; }
}

method Main() {
    // Test 0 BU
    var S0 : set<int> := {} ;
    var R0 := part2BU( S0 ) ;
    var E0 := {({},{})} ;
    if R0 != E0 { print "Test 0 BU fails. Got ", R0, " but expected ", E0, "\n" ; }
    else { print "Test 0 BU passes. Got ", R0, "\n" ; }

    // Test 1 BU
    var S1 : set<string> := { "fred" } ;
    var R1 := part2BU( S1 ) ;
    var E1 := {({"fred"},{ }), ({ },{"fred"})} ;
    if R1 != E1 { print "Test 1 BU fails. Got ", R1, " but expected ", E1, "\n"; }
    else { print "Test 1 BU passes. Got ", R1, "\n" ; }

    // Test 2 BU
    var S2 : set<string> := { "hello", "world" } ;
    var R2 := part2BU( S2 ) ;
    var E2 := { ({ "hello", "world" },{ }),
                ({ "hello"}, { "world" }),
                ({ "world" }, { "hello" }),
                ({ },{ "hello", "world" }) } ;
    if R2 != E2 { print "Test 2 BU fails. Got ", R2, " but expected ", E2, "\n"; }
    else { print "Test 2 BU passes. Got ", R2, "\n" ; }


    // Test 0 TD
    R0 := part2TD( S0 ) ;
    if R0 != E0 { print "Test 0 TD fails. Got ", R0, " but expected ", E0, "\n" ; }
    else { print "Test 0 TD passes. Got ", R0, "\n" ; }

    // Test 1 TD
    R1 := part2TD( S1 ) ;
    if R1 != E1 { print "Test 1 TD fails. Got ", R1, " but expected ", E1, "\n"; }
    else { print "Test 1 TD passes. Got ", R1, "\n" ; }

    // Test 2 TD
    R2 := part2TD( S2 ) ;
    if R2 != E2 { print "Test 2 TD fails. Got ", R2, " but expected ", E2, "\n"; }
    else { print "Test 2 TD passes. Got ", R2, "\n" ; }
}