lpublic:
l List();
l // Create empty
List
l void Advance();
l /*Requires
|Rem|>0
l Ensures @Rem = x + Rem
l Prec = @Prec + x*/
l T Peek();
l /*Requires List is not
empty
l Ensures Peek = Rem.c*/
l int
Length_of_Rem();
l /*Requires True
l Ensures Length_of_Rem = |Rem| */
l void Reset();
l /*Requires True
l Ensures Prec is empty, Rem = @Prec +
@Rem*/
l…