*Structure 1.1:Abstract data type Natural_Number (p.17)
structure Natural_Number is
    objects: an ordered subrange of the integers starting at zero and ending 
	     at the maximum integer (INT_MAX) on the computer
    functions:
       for all x, y „¡ Nat_Number; TRUE, FALSE „¡ Boolean
       and where +, -, <, and == are the usual integer operations.
       Nat_No Zero ( )              ::=  0
       Boolean  Is_Zero(x)        ::= if (x) return FALSE
                                    else return TRUE
       Nat_No Add(x, y)           ::= if ((x+y) <= INT_MAX) return x+y 
                                    else return INT_MAX
       Boolean Equal(x,y)         ::= if (x== y) return TRUE
                                    else return FALSE
       Nat_No Successor(x)      ::= if (x == INT_MAX) return x
                                    else return x+1
       Nat_No Subtract(x,y)      ::= if (x<y) return 0
                                    else return x-y
    end Natural_Number   

::= means "defined as"

§ë¼v¤ù 6 ¤§ 30