| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/while/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle Stm.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Statements % % 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 % % Version 1.0 25/12/07 Initial Version %------------------------------------------------------------------------------ Stm[V:TYPE+]: THEORY BEGIN IMPORTING AExp[V], BExp[V] Stm: DATATYPE BEGIN Assign(x:V,a:AExp) : Assign? Skip : Skip? Sequence(S1,S2:Stm) : Sequence? Conditional(b:BExp,S1,S2:Stm) : Conditional? While(b:BExp,S1:Stm) : While? END Stm x: VAR V p: VAR pred[Stm] a: VAR AExp b: VAR BExp S,S1,S2: VAR Stm Stm_measure(S): RECURSIVE nat = cases S of Assign(x,a) : 0, Skip : 0, Sequence(S1,S2) : max(Stm_measure(S1),Stm_measure(S2))+1, Conditional(b,S1,S2) : max(Stm_measure(S1),Stm_measure(S2))+1, While(b,S1) : Stm_measure(S1)+1 endcases MEASURE S by << IMPORTING measure_induction[Stm,nat,Stm_measure,<] structural_induction: LEMMA (FORALL x,a: p(Assign(x,a))) AND p(Skip) AND (FORALL S1,S2: p(S1) AND p(S2) => p(Sequence(S1,S2))) AND (FORALL b,S1,S2: p(S1) AND p(S2) => p(Conditional(b,S1,S2))) AND (FORALL b,S1: p(S1) => p(While(b,S1))) IMPLIES (FORALL S: p(S)) END Stm ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28