% $Id: while_test_helpers.mod,v 1.6 2004/10/18 03:37:42 leavens Exp leavens $
% Helpers for testing for while programs
module while_test_helpers.

  accumulate while, test_helpers.

  %% adapter from test_helpers
  check 1 J :- checkC J.
  check 2 J :- checkE J.
  check_exists 1 J :- expectedC J L.
  check_exists 2 J :- expectedE J V L.

  %% Test for commands

  %% ``checkallC'' succeeds if all the command tests
  %% give their expected results.
  checkallC :- check_series 1 Total Failed, checkall_end Total Failed.

  %% ``checkC I'' succeeds if the Ith command test gives the expected result.
  checkC I :- runC I LS, expectedC I LS.

  %% ``runC I LS'' succeeds if the Ith command test, run on the initial store,
  %% produces the store represented by LS.
  runC I LS :- testC I C, meaningC C STO, show_store 0 STO LS.

  %% ``test I C'' succeeds if the Ith command test is C.
  testC I C :- testcaseC I C L.

  %% ``expected I L'' succeeds if the Ith command test's expected 
  %% final store is represented by L.
  expectedC I L :- testcaseC I C L.

  %% ``testcaseC I C L'' succeeds if the Ith command test is C
  %%  and its final store is represented by L.

  %% Expression tests

  %% ``checkallE'' succeeds if all the expression tests
  %% give their expected results.
  checkallE :- check_series 2 Total Failed, checkall_end Total Failed.

  %% ``checkE I'' succeeds if the Ith expression test gives
  %% the expected result. 
  checkE I :- runE I V S, show_store 0 S L, expectedE I V L.

  %% ``runE I V S'' succeeds if the Ith test, run on a store where
  %% location 1 is set to 3, produces the value V and store S.
  runE I V S :-
       testE I E,
       initial_store S0,
       (update S0 1 3 S1),
       meaningE E S1 V S.

  %% ``testE I E'' succeeds if the Ith expression test is E.
  testE I E :- testcaseE I E V L.

  %% ``expectedE I V L'' succeeds if the Ith expression test's value is V
  %% and if its final store is represented by L.
  expectedE I V L :- testcaseE I E V L.

  %% ``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.