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