// TODO: define a stack of odd numbers
class StackOdd 
{
    var s: seq<int>

    constructor ()
        ensures |s| == 0
    {
        s := [];
    }

    method pop() returns (n: int)
        requires 0 < |s|
        modifies this
    {
        var x := s[0];
        s := s[1..];
    }

    method push(n: int)
        modifies this
        ensures |s| == |old(s)| + 1
    {
        s := [n] + s;
    }

    method length() returns (n: nat)
        ensures n == |s|
    {
        return |s|;
    }


    method Main() 
    {
        var s1 := new StackOdd();
        s1.push(1);
        s1.push(2);
        var x := s1.pop();
        s1.push(3);
        var l := s1.length();
        assert l == 2;
    }
}