% $Id: while_test.mod,v 1.5 2004/10/17 06:39:03 leavens Exp $
module while_indirect_test.

  accumulate while_indirect_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).

  testcaseC 8 (semi (semi (assign (loc 5) (num 5))
                          (assign (loc 4) (num 4)))
                    (while (deref (loc 4))
                           (if (deref (loc 5))
                               (semi (assign (loc 4)
                                             (op sub (deref (loc 4)) (num 1)))
                                     (assign (indirect (deref (loc 4))) (deref (loc 4))))
			        skip)))
              (0::1::2::3::0::5::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).