Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Cobol/Test-Suite/SQL P/dml100-186/     Datei vom 4.1.2008 mit Größe 26 kB image not shown  

SSL horizontal_criteria.pvs   Interaktion und
PortierbarkeitPVS

 
%------------------------------------------------------------------------------
% horizontal_criteria.pvs
% ACCoRD v1.0
%
% This theory proposes criteria for horizontal separation for non-negative 
% times. These criteria guarantee independence and (implicit) coordination. 
%------------------------------------------------------------------------------

horizontal_criteria[D: posreal]: THEORY
BEGIN

  IMPORTING predicate_coordination_2D,horizontal[D]

  v,w       : VAR Vect2
  nzv       : VAR Nz_vect2
  sp        : VAR Sp_vect2
  ss        : VAR Ss_vect2
  vo,vi,
  nvo,nvi   : VAR Vect2
  eps,
  eps1,eps2 : VAR Sign

  R(sp):nnreal = sqrt(sqv(sp)-sq(D))/D

  R_eq_0 : LEMMA
    on_D?(sp) IFF
    R(sp) = 0

  R_gt_0 : JUDGEMENT
    R(ss) HAS_TYPE posreal
 
  R_symm : LEMMA
    R(-sp) = R(sp)

  sq_R_det : LEMMA 
    sp*v <= 0 IMPLIES
      (sq(sp*v) > sq(R(sp))*sq(det(sp, v)) IFF
       sp*v < R(sp)*det(sp,v) AND R(sp)*det(sp,v) < -(sp*v))

  Delta_sq_det: LEMMA   
    Delta(sp,nzv) > 0 IFF sq(R(sp))*sq(det(sp,nzv)) < sq(sp*nzv)

  Delta_sq_det_equality: LEMMA
    Delta(sp,nzv) = 0 IFF sq(R(sp))*sq(det(sp,nzv)) = sq(sp*nzv)

  Delta_zero_eps_line_equality: LEMMA
    Delta(sp,nzv) = 0 AND sp*nzv <= 0 
    IMPLIES 
    EXISTS (eps: Sign):
      eps*R(sp)*det(sp,nzv) = sp*nzv
      AND
      eps*det(sp,nzv) <= 0

  horizontal_solution: LEMMA
    horizontal_conflict?(sp,v)
    IFF
      (sp*v) < R(sp)*det(sp,v) AND R(sp)*det(sp,v) < -(sp*v)

  horizontal_criterion?(sp,eps)(v):bool =
    sp*v >= R(sp)*eps*det(sp,v) AND
    eps*det(sp,v) <= 0

  % horizontal_criterion_neg: LEMMA
  %   NOT horizontal_criterion?(sp,eps)(v) IMPLIES horizontal_criterion?(sp,eps)(-v)

  horizontal_criterion_scal: LEMMA
    FORALL (cc:nnreal): horizontal_criterion?(sp,eps)(v)
           IMPLIES
    horizontal_criterion?(sp,eps)(cc*v)

  horizontal_criterion?(sp,v) : MACRO bool =
    EXISTS (eps:Sign): horizontal_criterion?(sp,eps)(v)

  horizontal_criterion_eps : LEMMA
    horizontal_criterion?(sp,v) IMPLIES
    horizontal_criterion?(sp,sign(-det(sp,v)))(v)

  horizontal_criterion_symmetric: LEMMA
   horizontal_criterion?(sp,eps)(v) IFF
   horizontal_criterion?(-sp,eps)(-v)

  horizontal_criterion_eps_unique : LEMMA
    horizontal_criterion?(sp,eps1)(v) AND
    horizontal_criterion?(sp,eps2)(v) AND
    NOT (det(sp,v) = 0 AND sp*v >= 0)
    IMPLIES
    eps1=eps2

  horizontal_criterion_independence : THEOREM
    horizontal_criterion?(sp,v) IFF
    NOT horizontal_conflict?(sp,v)

  horizontal_criterion_sum_closed: LEMMA
    horizontal_criterion?(sp,eps)(v) AND
    horizontal_criterion?(sp,eps)(w)
    IMPLIES
    horizontal_criterion?(sp,eps)(v+w)

  horizontal_criterion_coordination : THEOREM
     horizontal_conflict?(sp,vo-vi) AND
     horizontal_criterion?(sp,eps)(nvo-vi) AND
     horizontal_criterion?(-sp,eps)(nvi-vo) 
     IMPLIES
     NOT horizontal_conflict?(sp,nvo-nvi)

  horizontal_sep_dir: LEMMA
    horizontal_dir?(sp,v,eps)
    IMPLIES
      horizontal_sep_dir_at?(sp,v,0,eps)

  horizontal_exit_independence: THEOREM
    horizontal_exit?(sp,v) OR Delta(sp,v) <= 0
    IFF
      NOT horizontal_conflict?(sp,v)

  horizontal_exit_coordination: THEOREM
    horizontal_conflict?(sp,vo-vi) AND
    horizontal_exit?(sp,nvo-vi) AND
    horizontal_exit?(-sp,nvi-vo) 
    IMPLIES
      NOT horizontal_conflict?(sp,nvo-nvi)

END horizontal_criteria

98%


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.0Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤

*Eine klare Vorstellung vom Zielzustand




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.