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.1 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.
|
