Package arithtest

Import "arithmetic".

%% The following functions are provided for convenience.

Expect 
  intToBinary: Integer -> [Integer]
     %: intToBinary(n) is the binary equivalent of
     %: nonnegative integer n.
     ;

  binaryToInt: [Integer] -> Integer
     %: binaryToInt(x) is the integer that binary
     %: list x stands for.
%Expect

Define 
  case intToBinary (0)     = []
  case intToBinary (2*n)   = 0 :: intToBinary(n)
  case intToBinary (2*n+1) = 1 :: intToBinary(n)
%Define

Example
  intToBinary(12) = [0,0,1,1]
%Example

Define 
  case binaryToInt([])   = 0
  case binaryToInt(0::x) = 2*binaryToInt(x)
  case binaryToInt(1::x) = 2*binaryToInt(x) + 1
%Define

Example
  binaryToInt([0,0,1,1]) = 12
%Example


%% Note: $(x) is x converted to a string.  It is similar
%% to x.tostring() in Java.

Define TestInc(n). =
  Let x = intToBinary(n).
  Let y = inc(x).
  Let z = binaryToInt(y).

  If z == n + 1 then
    Writeln["inc works for ", $(n)].
  else
    Writeln["***inc(", $(n), ") = ", $(z)].
    Writeln["+++inc(", $(x), ") = ", $(y)].
  %If
%Define

Execute
  TestInc(0).
  TestInc(1).
  TestInc(2).
  TestInc(31).
  TestInc(64).  

  %% ***** Add more tests
%Execute

%Package