Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: top.pvs Sprache: PVS

Original von: PVS^©

%------------------------------------------------------------------------------
% 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.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.