%------------------------------------------------------------------------------
% Top 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
%
% The Programming Language "while" has been parameterized over the type of
% variables (V); this is so that variable renaming can be made easier when
% needed.
%
% Version 1.0 25/12/07 Initial Version
%------------------------------------------------------------------------------
top[V:TYPE+]: THEORY
BEGIN
IMPORTING
list_props_aux, % Extras for prelude library
State[V], % States and assignment
AExp[V], % Arithmetic Expressions and their evaluation function
BExp[V], % Boolean Expressions and their evaluation function
Stm[V], % Statements of While and structural induction principle
Cont[V], % Partial functions from State to State, and their order
direct[V], % A direct denotational semantics for While
continuation[V],% A continuation semantics for While
congruence[V], % An equivalence proof (direct & continuation)
sos[V], % A Structural Operational Semantics
direct_sos[V], % An equivalence proof (direct & sos)
compiler[V], % A compiler
Instruction[V], % Instruction set for an abstract machine
am[V], % An abstract machine
bisimulation[V],% An equivalence proof (sos & am/compiler)
axiomatic[V], % An Axiomatic Semantics (Sound and Complete rwt sos)
natural[V] % A natural semantics and its equivalence to sos
END top
¤ 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.
|
