Quelle tdiv.pvs Sprache: PVS

tdiv: THEORY

%------------------------------------------------------------------------
% Defines natural and integer division  (Number Theory Style)
%
% There is no universally agreed semantics for integer division for a
% negative argument.  For a negative argument, division can be defined
% with truncation towards or away from zero.  The definition in this
% theory truncates away from zero (i.e. div(-7,3) = -3).  This is is the
% approach used in most number theory books.  This approach has the
% advantage that div(i,m) = the greatest integer less than i/m.  The
% alternate approach (i.e. truncation towards zero: div(-7,3) = -2) is
% simpler to compute because div(-i,m) = -div(i,m) under that
% definition.  It is the method defined in tha Ada reference manual.
%
% To prevent confusion with other "div", this one has been renamed "tdiv"
%
%
%% AUTHOR
% ------
%
%   Ricky W. Butler
%   Mail Stop 130      fax: (804) 864-4234
%   NASA Langley Research Center    phone: (804) 864-6198
%   Hampton, Virginia 23681-0001
%------------------------------------------------------------------------

  BEGIN

  i,k: VAR int
  n: VAR nat
  m: VAR posnat
  j: VAR nonzero_integer
  x: VAR real
  negi,ngi2: VAR negint

  tdiv(i,j): integer = floor(i/j)

  sgn(x): int = IF x >= 0 THEN 1 ELSE -1 ENDIF

  JUDGEMENT tdiv(n,m) HAS_TYPE nat
  JUDGEMENT tdiv(negi,m) HAS_TYPE  negint
  JUDGEMENT tdiv(negi,ngi2) HAS_TYPE  nonneg_int
  JUDGEMENT tdiv(m,negi) HAS_TYPE  negint

  tdiv_nat:        LEMMA tdiv(n,m) = IF n>=m THEN 1 + tdiv(n-m, m) ELSE 0 ENDIF

  tdiv_neg_d:   LEMMA tdiv(i,-j) = IF integer_pred(i/j) THEN
          -tdiv(i,j)
        ELSE
          -tdiv(i,j)-1
        ENDIF

  tdiv_neg:   LEMMA tdiv(-i,j) = IF integer_pred(i/j) THEN
                 -tdiv(i,j)
        ELSE
          -tdiv(i,j)-1
        ENDIF

  tdiv_def:      THEOREM tdiv(i,m) =
                           IF i >= m THEN 1 + tdiv(i-m, m)
                           ELSIF i >= 0 THEN 0
                           ELSIF integer_pred(i/m) THEN -tdiv(-i,m)
                           ELSE
                             -1 - tdiv(-i,m)
                           ENDIF

  tdiv_sgn:        LEMMA tdiv(i,-j) = tdiv(-i,j)

  tdiv_value:      LEMMA i >= k*j AND i < (k+1)*j IMPLIES
                          tdiv(i,j) = k

% ================== tdiv for special values =============================

  tdiv_zero:   LEMMA tdiv(0,j) = 0

  tdiv_one:   LEMMA abs(j) > 1 IMPLIES tdiv(1,j) =
                           IF j >= 0 THEN 0 ELSE -1 ENDIF

  tdiv_eq_arg:   LEMMA tdiv(j,j) = 1

  tdiv_by_one:   LEMMA tdiv(i,1) = i

  tdiv_eq_0:   LEMMA tdiv(i,j) = 0 IMPLIES i = 0 OR
                    (sgn(i) = sgn(j) AND abs(i) < abs(j))

  tdiv_lt:   LEMMA abs(i) < abs(j) IMPLIES
                          tdiv(i,j) = IF i = 0 OR sgn(i) = sgn(j) THEN 0
                                     ELSE -1
                                     ENDIF

  tdiv_parity:   LEMMA sgn(i) = sgn(j) IMPLIES tdiv(i,j) >= 0

  tdiv_parity_neg: LEMMA sgn(i) /= sgn(j) IMPLIES tdiv(i,j) <= 0

  tdiv_smaller:    LEMMA m * tdiv(n,m) <= n

  tdiv_abs:        LEMMA abs(tdiv(i,j)) =
                          IF integer_pred(i/j) OR sgn(i) = sgn(j) THEN
                             tdiv(abs(i),abs(j))
                          ELSE tdiv(abs(i),abs(j)) + 1
                          ENDIF

  tdiv_max:        LEMMA abs(j) * abs(tdiv(i,j)) <= abs(i) + abs(j)

% ================== tdiv over addition =================================

  tdiv_multiple:      LEMMA tdiv(k*j,j) = k

  tdiv_sum:           LEMMA tdiv(i+k*j,j) = tdiv(i,j) + k

END tdiv

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.