products/sources/formale Sprachen/PVS/ACCoRD/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: horizontal_cr.pvs   Sprache: PVS

Original von: PVS©
%------------------------------------------------------------------------------
% horizontal_cr.pvs
% ACCoRD v.1.0
% Horizontal resolution algorithms
%------------------------------------------------------------------------------

horizontal_cr[D:posreal] : THEORY

BEGIN

  IMPORTING gs_line[D], 
            trk_line[D], 
            opt_line[D]

  sp      : VAR Sp_vect2
  vo,vi,
  nvo     : VAR Vect2
  eps     : VAR Sign

  %------------%
  % ALGORITHMS %
  %------------%

  horizontal_cr?(sp,vo,vi,eps)(nvo) : bool =
    gs_line_eps?(sp,vo,vi,eps)(nvo) OR
    trk_line_eps?(sp,vo,vi,eps)(nvo) OR
    opt_line_eps?(sp,vo,vi,eps)(nvo) 

  %--------------------------%
  % LEMMAS                   %
  %--------------------------%

  horizontal_cr_is_line_solution: THEOREM
    horizontal_cr?(sp,vo,vi,eps)(nvo)
    IMPLIES 
      line_solution?(sp,nvo-vi,eps)

END horizontal_cr

¤ Dauer der Verarbeitung: 0.12 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff