%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
