| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/fault_tolerance/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 kB |
|
SSL top.pvs Sprache: 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.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28