Quelle  AExp.pvs

%------------------------------------------------------------------------------
% Arithmetic Expressions
%
% All references are to HR and F Nielson "Semantics with Applications:
% A Formal Introduction", John Wiley & Sons, 1992. (revised edition
% available: http://www.daimi.au.dk/~hrn )
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            25/12/07  Initial Version
%------------------------------------------------------------------------------

AExp[V:TYPE+]: THEORY

BEGIN

  IMPORTING State[V]

  AExp: DATATYPE  
  BEGIN
    N(n:int)        : N?
    V(x:V)          : V?
    Add(a1,a2:AExp) : Add?
    Sub(a1,a2:AExp) : Sub?
    Mul(a1,a2:AExp) : Mul?
  END AExp

  s: VAR State

  A(a:AExp) : RECURSIVE [State->int] =
    LAMBDA s: cases a of
                      N(n) : n,
                      V(x) : s(x),
                      Add(a1,a2) : A(a1)(s) + A(a2)(s),
                      Sub(a1,a2) : A(a1)(s) - A(a2)(s),
                      Mul(a1,a2) : A(a1)(s) * A(a2)(s)
                    endcases
                    MEASURE a by <<

END AExp