ADT Name  Describe of data;  Operations;End ADT

Operations description:Name(parameter list)  Input:     data used to input  Output:   data used to output  Pre-condition:  if the condiont my not be satisfied, the operation may not be correct   Post-condition:  The status after the operation be executed

ADT Bigint    Data        n: 0..2^54-1    Operations:                addone            Pre-condition:     n+1<2^54;            Post-condition:    n=n+1;                 subone             Pre-condition:    n>0;             Post-condition:   n=n-1;                  mult(x,y)             Input:   (x:Bigint);             Output: (y:Bigint);             Pre-condition:  n*x.n<2^54;             Post-condition: y.n=n*x.n;End ADT