%------------------------------------------------------------------------------
% A Direct Semantics for the While Language
%
% 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
%------------------------------------------------------------------------------

direct[V:TYPE+]: THEORY

BEGIN

  IMPORTING AExp[V], BExp[V], State[V], Stm[V], Cont[V],
            scott@partial_function_props[State,State],
            scott@fixpoints[Cont,(sq_le)]

  s: VAR State
  S: VAR Stm
  c: VAR Cont

  SS(S) : RECURSIVE Cont =
    cases S of
      Assign(x,a)          : (LAMBDA s: up(assign(x,A(a))(s))),
      Skip                 : (LAMBDA s: up(s)),
      Sequence(S1,S2)      : SS(S2) o SS(S1),
      Conditional(b,S1,S2) : conditional(B(b),SS(S1),SS(S2)),
      While(b,S1)          : fix(LAMBDA c: conditional(B(b), c o SS(S1),
                                           LAMBDA s: up(s)))
    endcases MEASURE S by <<

END direct