% Evaluation semantics for arithmetic expressions,
% adapted from M. Hennessy: The Semantics of
% Programming Languages (Wiley, 1990).
module arith.

  accumulate arith_abstract_syntax.
  
  % auxilliary semantic relations
  local	ap	operator -> int -> int
			 -> int -> o.

  % the evalsto relation
  
       (evalsto (num N) N).
  
       ((evalsto E1 V1), (evalsto E2 V2),
        (ap Oper V1 V2 Ans))
  => % ----------------------------------
       (evalsto (op Oper E1 E2) Ans).
  
   (ap add N1 N2 Ans) :- Ans is N1 + N2.
   (ap sub N1 N2 Ans) :- Ans is N1 - N2.
   (ap mult N1 N2 Ans) :- Ans is N1 * N2.