8
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…