Quelle bisimulation.pvs Sprache: PVS

%------------------------------------------------------------------------------
% The Equivalence of a Compiler/Abstract Machine
%         and 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
%------------------------------------------------------------------------------

bisimulation[V:TYPE+]: THEORY

BEGIN

  IMPORTING compiler[V], am[V], sos[V]

  x: VAR V
  a: VAR AExp
  b: VAR BExp
  n,m: VAR nat
  pn: VAR posnat
  e: VAR list[int]
  s,s0,s1: VAR State
  S: VAR Stm
  sc,sc0,sc1: VAR sos.Config
  ac,ac0,ac1,ac2: VAR am.Config

  correct_AExp: LEMMA EXISTS n: am.tr(n)((CA(a),e,s),(null,cons(A(a)(s),e),s))
                                                                     % N&N 3.18
  correct_BExp: LEMMA EXISTS n: am.tr(n)((CB(b),e,s),(null,cons(B(b)(s),e),s))
                                                                     % N&N 3.19

  eq_AExp: LEMMA am.tr(n)((CA(a),e,s),(null,cons(A(a)(s),e),s)) AND
                 am.tr(m)((CA(a),e,s),ac) AND
                 null?(ac`1) =>
                 n = m AND ac`2 = cons(A(a)(s),e) AND ac`3 = s

  AExp_steps: LEMMA am.tr(n)((CA(a),e,s),(null,cons(A(a)(s),e),s)) => n >= 1

  AExp_e: LEMMA am.tr(n)((CA(a),e,s),(null,cons(A(a)(s),e),s)) AND
                      pn <= n AND am.tr(pn)((CA(a),e,s),ac) =>
                      length(ac`2) >= 1+length(e)

  eq_BExp: LEMMA am.tr(n)((CB(b),e,s),(null,cons(B(b)(s),e),s)) AND
                 am.tr(m)((CB(b),e,s),ac) AND
                 null?(ac`1) =>
                 n = m AND ac`2 = cons(B(b)(s),e) AND ac`3 = s

  BExp_steps: LEMMA am.tr(n)((CB(b),e,s),(null,cons(B(b)(s),e),s)) => n >= 1

  BExp_e: LEMMA am.tr(n)((CB(b),e,s),(null,cons(B(b)(s),e),s)) AND
                      pn <= n AND am.tr(pn)((CB(b),e,s),ac) =>
                      length(ac`2) >= 1+length(e)

;
  ~(sc,ac): bool
    = IF terminal?(sc)
      THEN ac`1 = null[Instruction] AND ac`2 = null[int] AND s1(sc) = ac`3
      ELSE ac`1 = CS(S(sc))         AND ac`2 = null[int] AND s(sc)  = ac`3
      ENDIF

  sos_step: LEMMA
     sos.I(S,s) ~ ac0 =>
     EXISTS pn,ac1: sos.step(S,s) ~ ac1 AND am.tr(pn)(ac0,ac1)

  sos_steps: LEMMA sos.tr(n)(sos.I(S,s0),T(s1)) =>
                   EXISTS m: am.tr(m)((CS(S),null[int],s0),
                                      (null[Instruction],null[int],s1))

  am_step1: LEMMA sos.I(S,s) ~ ac AND
                  sos.step(S,s) ~ ac1 =>
                  EXISTS pn: am.tr(pn)(ac,ac1) AND
                  FORALL n,ac2: n <= pn AND am.tr(n)(ac,ac2) =>
                                (null?(ac2`2) IFF (n=0 OR n=pn))

  am_steps: LEMMA                                                    % N&N 3.27
    am.tr(m)((CS(S),null[int],s0),(null[Instruction],null[int],s1)) =>
    EXISTS n: sos.tr(n)(sos.I(S,s0),T(s1))

  bisimulation: LEMMA M(CS(S)) = SS(S)                               % N&N 3.28

END bisimulation

quality97%

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.