% $Id: classicjava_test_helpers.mod,v 1.3 2007/05/28 18:58:18 leavens Exp $
% Helpers for testing classicjava programs
module classicjava_test_helpers.

  accumulate classicjava, classicjava_testct, test_helpers.

  %% adapters from test_helpers.
  check 1 J :- checkE J.
  check_exists 1 J :- expectedE J V L.

  %% Expression tests

  %% ``checkallE'' succeeds if all the expression tests
  %% give their expected results.
  checkallE :- check_series 1 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 (object "Object" empty_f_fun) S L, 
              expectedE I V L.

  %% ``runE I V S'' succeeds if the Ith test, 
  %% in a store where location 0 is set to (object "Object" empty_f_fun),  
  %% produces the value V and store S.
  runE I V S :-
       testE I E,
       example CT,
       initial_store S0,
       (update S0 0 (object "Object" empty_f_fun) S1),
       meaningE CT 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.

end