|
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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
