% $Id: classicjava_tests.mod,v 1.6 2007/05/28 21:28:59 leavens Exp $
% Testing for classic java programs
%
% You can run all of the tests by executing the query.
%    checkall.
%
% See the module classicjava_test_helpers for other helpers, like run.
%
module classicjava_tests.
  accumulate classicjava_test_helpers.

  %        num expression  value   store list
  testcaseE 1 (new "Blue") (ref 1) L.

  testcaseE 2 (new "Blue") (ref 1)
     ((object "Object" empty_f_fun)
      ::(object "Blue" empty_f_fun)::nil).

  testcaseE 3 (fassign (new "Stack") "elems" (new "Nil")) (ref 2)
     ((object "Object" empty_f_fun)
      ::(object "Stack" (f_fun_extend "elems" (ref 2) FMap))
      ::(object "Nil" empty_f_fun)
      ::nil).

  testcaseE 4 (fassign (new "Stack") "elems" (new "Nil")) (ref 2)
     ((object "Object" empty_f_fun)
      ::(object "Stack" (f_fun_extend "elems" (ref 2)
                            (f_fun_extend "elems" nullref empty_f_fun)))
      ::(object "Nil" empty_f_fun)
      ::nil).

  testcaseE 5 (mcall (new "Stack") "init" nil) (ref 1)
     ((object "Object" empty_f_fun)
      ::(object "Stack" (f_fun_extend "elems" (ref 2)
                            (f_fun_extend "elems" nullref empty_f_fun)))
      ::(object "Nil" empty_f_fun)
      ::nil).

  testcaseE 6 (dot (mcall (new "Stack") "init" nil) "elems") (ref 2)
     ((object "Object" empty_f_fun)
      ::(object "Stack" (f_fun_extend "elems" (ref 2)
                            (f_fun_extend "elems" nullref empty_f_fun)))
      ::(object "Nil" empty_f_fun)
      ::nil).

  testcaseE 7 (mcall (mcall (new "Stack") "init" nil) "isEmpty" nil) (ref 3)
     ((object "Object" empty_f_fun)
      ::(object "Stack" (f_fun_extend "elems" (ref 2)
                            (f_fun_extend "elems" nullref empty_f_fun)))
      ::(object "Nil" empty_f_fun)
      ::(object "True" empty_f_fun)
      ::nil).

  testcaseE 8 (mcall
                (mcall (new "Stack") "init" nil)
                "push" ((new "Blue")::nil))
     (ref 1)
     ((object "Object" empty_f_fun)
      ::(object "Stack" (f_fun_extend "elems" (ref 4) OldFMap))
      ::(object "Nil" empty_f_fun)
      ::(object "Blue" empty_f_fun)
      ::(object "Cons" (f_fun_extend "cdr" (ref 2)
                         (f_fun_extend "car" (ref 3) OldConsMap)))
      ::nil).

  testcaseE 9 (mcall
                (mcall
                  (mcall (new "Stack") "init" nil)
                 "push" ((new "Blue")::nil))
               "isEmpty" nil)
     (ref 5)
     ((object "Object" empty_f_fun)
      ::(object "Stack" (f_fun_extend "elems" (ref 4) OldFMap))
      ::(object "Nil" empty_f_fun)
      ::(object "Blue" empty_f_fun)
      ::(object "Cons" (f_fun_extend "cdr" (ref 2)
                         (f_fun_extend "car" (ref 3) OldConsMap)))
      ::(object "False" empty_f_fun)
      ::nil).

  testcaseE 10 null nullref 
     ((object "Object" empty_f_fun)
      ::nil).

  testcaseE 11
        (semi null
              (mcall
                (mcall
                  (mcall (new "Stack") "init" nil)
                 "push" ((new "Blue")::nil))
               "isEmpty" nil))
     (ref 5)
     ((object "Object" empty_f_fun)
      ::(object "Stack" (f_fun_extend "elems" (ref 4) OldFMap))
      ::(object "Nil" empty_f_fun)
      ::(object "Blue" empty_f_fun)
      ::(object "Cons" (f_fun_extend "cdr" (ref 2)
                         (f_fun_extend "car" (ref 3) OldConsMap)))
      ::(object "False" empty_f_fun)
      ::nil).

  testcaseE 12
     (cast (cn "Stack") (mcall (new "ColoredStack") "init" nil))
     (ref 1)
     ((object "Object" empty_f_fun)
      ::(object "ColoredStack" (f_fun_extend "color" (ref 3)
                                 (f_fun_extend "elems" (ref 2) OldFMap)))
      ::(object "Nil" empty_f_fun)
      ::(object "Blue" empty_f_fun)
      ::nil).

  testcaseE 13
     (mcall
       (cast (cn "Stack") (mcall (new "ColoredStack") "init" nil))
      "push" ((new "Blue")::nil))
     (ref 1)
     ((object "Object" empty_f_fun)
      ::(object "ColoredStack" (f_fun_extend "elems" (ref 5)
                                (f_fun_extend "color" (ref 3)
                                 OldFMap)))
      ::(object "Nil" empty_f_fun)
      ::(object "Blue" empty_f_fun)
      ::(object "Blue" empty_f_fun)
      ::(object "Cons" (f_fun_extend "cdr" (ref 2)
                         (f_fun_extend "car" (ref 4) OldConsMap)))
      ::nil).

  testcaseE 14
     (cast (cn "Blue")
      (mcall 
        (mcall
          (cast (cn "Stack") (mcall (new "ColoredStack") "init" nil))
         "push" ((new "Blue")::nil))
      "top" nil)
     )
     (ref 4)
     ((object "Object" empty_f_fun)
      ::(object "ColoredStack" (f_fun_extend "elems" (ref 5)
                                (f_fun_extend "color" (ref 3)
                                 OldFMap)))
      ::(object "Nil" empty_f_fun)
      ::(object "Blue" empty_f_fun)
      ::(object "Blue" empty_f_fun)
      ::(object "Cons" (f_fun_extend "cdr" (ref 2)
                         (f_fun_extend "car" (ref 4) OldConsMap)))
      ::nil).

end