| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ints/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle rem.pvs Sprache: PVS |
|||||||||
|
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: r.w.butler@larc.nasa.gov % 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.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28