% $Id: while_test.mod,v 1.5 2004/10/17 06:39:03 leavens Exp $
% Testing for while programs
%
% You can run all of the tests by executing the query.
%    checkall.
% You can run all of the command tests by executing the query.
%    checkallC.
% You can run all of the expression tests by executing the query.
%    checkallE.
%
% See the module while_test_helpers for other helpers, like run.
%
module while_test.

  accumulate while_test_helpers.

  %% ``testcaseC I C L'' succeeds if the Ith command test is C
  %%  and its final store is represented by L.
  testcaseC 1 (semi (assign (loc 1) (num 1))
                    (assign (loc 2) (num 2)))
              (0::1::2::nil).

  testcaseC 2 (semi (assign (loc 1) (num 1))
                    (if (deref (loc 1))
                        (assign (loc 1) (num 3))
                        (assign (loc 1) (num 4))))
              (0::3::nil).

  testcaseC 3 (semi (assign (loc 1) (num 1))
                    (while (deref (loc 1))
                           (assign (loc 1) (num 0))))
              (0::0::nil).

  testcaseC 4 (semi (assign (loc 1) (num 1))
                    (if (deref (loc 1))
                        (assign (loc 1) (num 3))
                        (assign (loc 1) (num 4))))
              (0::3::nil).

  testcaseC 5 (semi (assign (loc 1) (num 0))
                    (if (deref (loc 1))
                        (assign (loc 1) (num 3))
                        (assign (loc 1) (num 4))))
              (0::4::nil).

  testcaseC 6 (semi (assign (loc 1) (num 10))
                    (while (deref (loc 1))
                           (assign (loc 1) (op sub (deref (loc 1)) (num 1)))))
              (0::0::nil).

  testcaseC 7 (while (num 0)
                     (while (num 1) (exp (num 1))))
              (nil).

  %% Expression tests

  %% ``testcaseE I E V L'' succeeds if the Ith expression test is E,
  %% its expected value is V, and final store is represented by L.

  testcaseE 1 (deref (loc 1))
              3 L.

  testcaseE 2 (op sub (deref (loc 1)) (deref (loc 0)))
              3 L.

  testcaseE 3 (op mult (deref (loc 1)) (op add (deref (loc 0)) (num 3)))
              9 (0::3::nil).

  testcaseE 4 (op sub (deref (loc 1)) (deref (loc 0)))
              3 (0::3::nil).