Top File of PVS while Library

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

The tag identifies links that are outside the NASA domain