proc main() {
    assert(y >= 1 & x >= 0 & x == x0);
    assert(y >= 1 & x >= 0 & x == x0 & x*y == x0*y);    % Implied (VC 1)
    s := x * y;
    assert(y >= 1 & x >= 0 & x == x0 & s == x0*y);
    t := x ;
    assert (y >= 1 & x >= 0 & t == x0 & s == x0*y); % Asn

    while y > 1 do {
        assert (y >= 1 & x >= 0 & t == x0 & s == x0*y & y > 1); % Inv & guard
        y := y - 1;
        assert (y >= 0 & x >= 0 & t == x0 & s == x0*(y+1) & y > 0) % Asn
        x := t;
        assert (!!) % Asn

        while !(x == 0) do {
            assert(!! & !(x==0)); % Inv & guard

            x := x - 1;
            s := s - 1;

            assert(!!);
        };
        assert(!! & x == 0); % Partial While
        assert(y >= 1 & x >= 0 & t == x0 & s == x0*y);
    };

    assert(y >= 1 & x >= 0 & t == x0 & s == x0*y & !(y > 1)); % Partial While
    assert(s == x0); % Implied (VC 3)
}