Quelle  Stm.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