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

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Cobol/Test-Suite/SQL M/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 4.1.2008 mit Größe 4 kB

Quelle line_solutions.pvs Sprache: PVS

%------------------------------------------------------------------------------
% line_solutions.pvs
% ACCoRD v1.0
%
% Line solutions are a special case of horizontal solutions. They are
% are tangent to the protected zone. In this case, eps determines the
% side of the protected zone that the is touched.
% It is proven that line solutions satisfy independence and (implicit)
% coordination.
%------------------------------------------------------------------------------

line_solutions[D: posreal]: THEORY
BEGIN

  IMPORTING horizontal_criteria[D],
           vectors@linear_transformations_2D

  sp,s2         : VAR Sp_vect2
  s,v,v1,v2,v3,
  vo,vi,nvo,nvi : VAR Vect2
  eps,eps1,eps2 : VAR Sign
  t,t2,t3    : VAR real
  nzv,nzv1,nzv2 : VAR Nz_vect2
  k             : VAR real
  pk            : VAR posreal
  tt  : VAR nnreal

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

  line_solution_dot_neg : LEMMA
    line_solution?(sp,v,eps) IMPLIES
    sp*v <= 0

  line_solution_sep_dot_negative: LEMMA
    sqv(sp) > sq(D) AND v /= zero AND
    line_solution?(sp,v,eps) IMPLIES
    sp*v < 0

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

  line_solution_on_D: LEMMA
    on_D?(s) IMPLIES
    line_solution?(s,eps*perpR(s),eps)

  on_D_line : LEMMA
    on_D?(s) AND s*v = 0 IMPLIES line_solution?(s,v)

  line_solution_scal : LEMMA
    line_solution?(sp,v,eps) IFF line_solution?(sp,pk*v,eps)

  line_solution_zero_eps : LEMMA
    line_solution?(sp,zero,eps)

  line_solution_zero : LEMMA
    line_solution?(sp,zero)

  line_solution_Delta: LEMMA
    line_solution?(sp,v) IFF Delta(sp,v) = 0 AND horizontal_entry?(sp,v)

  det_neq_0 : LEMMA
    line_solution?(sp,nzv) IMPLIES
    det(sp,nzv) /= 0

  eps_line(s,v): Sign = -sign(det(s,v))

  line_solution_eps : LEMMA
    line_solution?(sp,nzv,eps) IMPLIES
    eps = eps_line(sp,nzv)

  line_solution_eps_line : LEMMA
    line_solution?(sp,v) IMPLIES
    line_solution?(sp,v,eps_line(sp,v))

  line_solution_meets_horizontal_criterion: LEMMA
    line_solution?(sp,v,eps) IMPLIES
    horizontal_criterion?(sp,eps)(v)

  line_solution_independence : THEOREM
    line_solution?(sp,v) IMPLIES
    NOT horizontal_conflict_ever?(sp,v)

  line_solution_invariant: LEMMA
    sign(-(sp*v)) = sign(-((sp+t*v)*v)) IMPLIES
   (line_solution?(sp,v) IMPLIES line_solution?(sp+t*v,v))

  line_solution_rewrite: LEMMA line_solution?(sp,nzv) IFF
    EXISTS (tt): on_D?(sp+tt*nzv) AND (sp+tt*nzv)*nzv = 0

  line_solution_det: LEMMA line_solution?(sp,v,eps)
    IFF (-eps*det(sp,v) = D*norm(v) AND horizontal_entry?(sp,v))

  line_solution_scal_unique: LEMMA
    line_solution?(sp,nzv1,eps) AND line_solution?(sp,nzv2,eps)
    AND
    sqv(sp) > sq(D)
    IMPLIES
    EXISTS (pk:posreal): nzv1 = pk*nzv2

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

  line_solution_along_line: LEMMA
    det(v1,v2) /= 0 IMPLIES
    LET t1 = ((-eps)*D*norm(v2) - det(sp,v2))/det(v1,v2) IN
    (sp + t1*v1)*v2 <= 0 IMPLIES line_solution?(sp + t1*v1,v2,eps)

END line_solutions

quality100%

¤ Dauer der Verarbeitung: 0.13 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.