Details About PVS While Library

     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


    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



 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 )