products/sources/formale Sprachen/C/Lyx/po/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: rem.pvs   Sprache: Unknown

rem: THEORY
%------------------------------------------------------------------------
% Defines remainder (rem)   (Ada Style)
%
% This version of "rem" is based upon the Ada Reference Manual's
% definition.  These depend upon the use of a division theory that truncates
% toward zero on a negative argument.  
%
% AUTHORS
% -------
%   Ricky W. Butler       email: [email protected]
%   Mail Stop 130      fax: (804) 864-4234
%   NASA Langley Research Center    phone: (804) 864-6198
%   Hampton, Virginia 23681-0001
%
% NOTE: There is now a "rem" defined in the prelude that is different
%       from this one.
% 
%------------------------------------------------------------------------

  BEGIN
 
  IMPORTING div
 
  i,k,cc: VAR int
  m: VAR posnat
  n,a,b,c: VAR nat   

  j: VAR nonzero_integer

% ======================= define rem(i,m) ========================

  ml1: LEMMA n -  m * div(n,m) < m
  ml3: LEMMA abs(i -  m * div(i,m)) < m

  rem(i,j): {k| abs(k) < abs(j)} =  i - j*div(i,j)

  rem_neg:        LEMMA rem(-i,j) = -rem(i,j)

  rem_neg_d:      LEMMA rem(i,-j) = rem(i,j)

  rem_even:       LEMMA integer_pred(i/j) IMPLIES rem(i,j) = 0

  rem_eq_arg:     LEMMA rem(j,j) = 0

  rem_zero:       LEMMA rem(0,j) = 0

  rem_lt:         LEMMA abs(i) < abs(j) IMPLIES 
                        rem(i,j) = i 

  rem_it_is:      LEMMA a = b + m*c AND b < m IMPLIES
                        b = rem(a,m)

  rem_eq_0:       LEMMA rem(i,j) = 0 IMPLIES integer_pred(i/j)

  rem_one:        LEMMA rem(1,j) = IF abs(j) = 1 THEN 0
                                   ELSE 1
                                   ENDIF
 
  JUDGEMENT rem(n,m) HAS_TYPE below(m)

  END rem

[ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ]