Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: sos.pvs Sprache: PVS

Original von: PVS^©

%------------------------------------------------------------------------------
% A Structural Operational Semantics
%
% 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
%------------------------------------------------------------------------------

sos[V:TYPE+]: THEORY

BEGIN

  IMPORTING State[V], AExp[V], BExp[V], Stm[V], Cont[V]

  S,S0,S1,S2: VAR Stm
  a: VAR AExp
  b: VAR BExp
  s,s0,s1,s2: VAR State
  i,j: VAR int
  x: VAR V
  n,k,k0,k1,k2: VAR nat

  Config: DATATYPE
  BEGIN
    I(S:Stm,s:State) : I?
    T(s1:State)      : T?
  END Config

  c,c0,c1,c2: VAR Config

  step(S,s): RECURSIVE [Config]
    = CASES S OF
        Assign(x,a)          : T(assign(x,A(a))(s)),
        Skip                 : T(s),
        Sequence(S1,S2)      : CASES step(S1,s) OF
                                 I(S11,s1) : I(Sequence(S11,S2),s1),
                                 T(s1)     : I(S2,s1) ENDCASES,
        Conditional(b,S1,S2) : IF B(b)(s) THEN I(S1,s) ELSE I(S2,s) ENDIF,
        While(b,S1)          : I(Conditional(b,Sequence(S1,S),Skip),s)
      ENDCASES MEASURE S BY <<

  terminal?(c):bool = T?(c)
  intermediate?(c):bool = I?(c)

  TConfig: TYPE = (terminal?)
  IConfig: TYPE = (intermediate?)

  TConfig_is_Config: JUDGEMENT TConfig SUBTYPE_OF Config
  IConfig_is_Config: JUDGEMENT IConfig SUBTYPE_OF Config

  tr(n)(c0,c): RECURSIVE bool
    = IF n=0 THEN c0=c
      ELSE I?(c0) AND CASES c0 OF I(S,s): tr(n-1)(step(S,s),c) ENDCASES ENDIF
      MEASURE n

  tr_add: LEMMA tr(k1+k2)(c0,c2) IFF EXISTS c1: tr(k1)(c0,c1) AND tr(k2)(c1,c2)
  tr_eq:  LEMMA tr(k)(c0,c1) AND tr(k)(c0,c2) => c1 = c2

  tr_split: LEMMA                                                    % N&N 2.19
     tr(k)(I(Sequence(S1,S2),s0),T(s2)) =>
     EXISTS s1,k1,k2:
       tr(k1)(I(S1,s0),T(s1)) AND tr(k2)(I(S2,s1),T(s2)) AND k1+k2=k

  tr_partial: LEMMA                                                  % N&N 2.21
     tr(k)(I(S1,s0),T(s1)) => tr(k)(I(Sequence(S1,S2),s0),I(S2,s1))

  tr_deterministic: LEMMA
     (tr(k1)(c,T(s1)) AND tr(k2)(c,T(s2))) => (k1 = k2 AND s1 = s2)

  SS(S) : Cont
    = lambda s:
        IF EXISTS n,s1: tr(n)(I(S,s),T(s1))
        THEN up(choose({s1 | EXISTS n: tr(n)(I(S,s),T(s1))}))
        ELSE bottom ENDIF

  SS_deterministic: LEMMA (EXISTS n: tr(n)(I(S,s),T(s1))) IFF SS(S)(s) = up(s1)
                                                                     % N&N 2.22

END sos

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.