//****************GLOBAL FUNCTION****************//

  // Determines if an input string is a valid number;
  function isNumberString(input:string):bool
    ^= (~input.empty) &                    //there is a value
       (forall x::input :- x.isDigit) &    //all the characters are digits
       (#input=1 |                         //the number is a single digit or
        input.head~=`0`)                  //... it doesn't contain leading zeros.
    assert result ==> (forall x::input :-x.isDigit);

//****************GLOBAL FUNCTION****************//

//****************AXIOM****************//

  axiom assert forall n:nat :- isNumberString(n.toString);

//****************AXIOM****************//

//****************CONSTRAINED TYPE****************//

  class NumericString ^= those a:string :- isNumberString(a);

//****************CONSTRAINED TYPE****************//

//****************SUPERCLASS****************//

deferred class Number ^=

interface
    build{};

    deferred function digit:nat;
end;
//****************SUPERCLASS****************//

//****************SUBCLASS****************//

class StringNumber ^= inherits Number
abstract
  const zero^=0;
  var number:NumericString;

  property assert forall d:StringNumber :- d+StringNumber{0}=d;
internal
 var num:nat;
 function number
   ^= num.toString;

confined
//****************STATIC FUNCTIONS****************//
  nonmember function toDigit(input:string,num:nat):nat
    pre forall x::input :- x.isDigit
    decrease #input
    ^= ([input.empty]: num,
        []: (let tail^=input.tail;
             assert forall y::tail :- y.isDigit;
             toDigit(tail,((num*10)+input.head.digit))
            )
       );
//****************STATIC FUNCTIONS****************//

interface
//****************CONSTRUCTORS****************//

  operator =(arg);

  // constructor that accepts a string that represents an natural
  build{input:string}
    pre isNumberString(input)
    inherits Number{}
    post number!=input
    via num!=toDigit(input,0)
    end;

  // constructor that accepts a natural number
  build{input:nat}
    inherits Number{}
    post number!=input.toString
    via num!=input
    end;
//****************CONSTRUCTORS****************//


//****************FUNCTIONS****************//
  define function digit:nat
    ^= toDigit(number,0)
    via value num
    end;

  redefine function toString:string
    ^= number
    via value num.toString
    end
    assert isNumberString(result);
//****************FUNCTIONS****************//


//****************SCHEMAS****************//
  schema !update(input:string)
    pre isNumberString(input)
    post number!=input
    via num!=toDigit(input,0)
    end;
//****************SCHEMAS****************//


//****************OPRERATORS****************//
  operator +(d:StringNumber):StringNumber
    ^= StringNumber{digit + d.digit}
    via value StringNumber{num+d.digit}
    end;
//****************OPRERATORS****************//
end;