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

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

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

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

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

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

Define TestInc(n:Integer). =
  Let x: [Integer] = intToBinary(n).
  Let y: [Integer] = inc(x).
  Let z: Integer   = 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