Quelle  continuation.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% A Continuation 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
%------------------------------------------------------------------------------

continuation[V:TYPE+]: THEORY

BEGIN

  IMPORTING AExp[V], BExp[V], State[V], Stm[V], Cont[V],
            scott@partial_function_props[State,State],
            scott@scott_continuity[Cont,Cont,(sq_le),(sq_le)],
            scott@scott_identity_continuity[Cont,(sq_le)],
            scott@scott_composition_continuity[Cont,Cont,Cont,
                                              (sq_le),(sq_le),(sq_le)],
            scott@pointwise_orders_aux[Cont,Cont],
            scott@fixpoints[scott_continuous[Cont,Cont,(sq_le),(sq_le)],
                            continuous_pointwise(sq_le,sq_le)]

  s:       VAR State
  a:       VAR AExp
  b:       VAR BExp
  c,c1,c2: VAR Cont
  f,g:     VAR scott_continuous[Cont,Cont,(sq_le),(sq_le)]
  x:       VAR V
  S:       VAR Stm

  identity_continuous:    LEMMA scott_continuous?(I[Cont])
  composition_continuous: LEMMA scott_continuous?(f o g)
  assign_continuous:      LEMMA
                    scott_continuous?(LAMBDA c: LAMBDA s: c(assign(x,A(a))(s)))
  conditional_continuous: LEMMA
                       scott_continuous?(LAMBDA c: conditional(B(b),f(c),g(c)))

  composition_conditional: LEMMA
    conditional(B(b),c o c1, c o c2) = c o conditional(B(b),c1,c2)

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

END continuation