products/Sources/formale Sprachen/Fortran/f90gl-1.2.15/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: floor_div_lems.pvs   Sprache: PVS

floor_div_lems: THEORY
BEGIN

  i,k: VAR int
  j: VAR nonzero_integer
  x: VAR real

%-------------------- following now in prelude --------------------
%
%  floor_val:   LEMMA i >= k*j AND i < (k+1)*j IMPLIES floor(i/j) = k 
%
%  floor_small: LEMMA  abs(i) < abs(j) IMPLIES
%                         floor(i/j) = IF i/j >= 0 THEN 0 ELSE -1 ENDIF
%
%  floor_eq_0:  LEMMA floor(x) = 0 IMPLIES x >= 0 AND x < 1


  n: VAR nat
  m: VAR posnat

  floor_small_nat: LEMMA n < m IMPLIES floor(n/m) = 0

  is_multiple: LEMMA integer_pred(i/j) = (EXISTS k: i = k*j)
 
END floor_div_lems

[ zur Elbe Produktseite wechseln0.19Quellennavigators  Analyse erneut starten  ]