Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Eigene Datei ansehen e.g. http://myserver.net/mysource.java Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/VDM/VDMSL/ACSSL/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: conv_oracle.mli Sprache: PVS

Original von: PVS^©

%------------------------------------------------------------------------------
% criteria_3D.pvs
% ACCoRD v.1.0
%------------------------------------------------------------------------------

criteria_3D[D,H:posreal] : THEORY
BEGIN

  IMPORTING vertical_criterion[D,H],
     horizontal_criterion_line[D]%,

  sp        : VAR Sp_vect3 % 3-D separation
  s,v,nv,
  nvo,nvi   : VAR Vect3
  vo,vi     : VAR Nzv2_vect3
  epsh,epsv : VAR Sign

  criterion_3D?(sp,v,epsh,epsv)(nv) : bool =
    (horizontal_sep?(sp) AND horizontal_criterion?(sp,epsh)(nv)) OR
    (vertical_criterion?(epsv)(sp,v)(nv) AND
     (horizontal_los?(sp) OR
      horizontal_criterion?(sp,epsh)(nv-v)))

  criterion_3D_independence : THEOREM
    conflict?(sp,v) AND
    criterion_3D?(sp,v,epsh,epsv)(nv)
    IMPLIES
      NOT conflict?(sp,nv)

  criterion_3D_coordination : THEOREM
    conflict?(sp,vo-vi) AND
    criterion_3D?(sp,vo-vi,epsh,epsv)(nvo-vi) AND
    criterion_3D?(-sp,vi-vo,epsh,-epsv)(nvi-vo) IMPLIES
    NOT  conflict?(sp,nvo-nvi)

END criteria_3D