| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ints/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 4 kB |
|
Quelle div.pvs Sprache: PVS |
|||||||||
|
div: THEORY
%------------------------------------------------------------------------ % Defines natural and integer division (Ada 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 toward zero (i.e. div(-7,3) = -2). This is % simpler to compute because div(-i,m) = -div(i,m) and is the % method defined in tha Ada reference manual. The alternate method % (i.e. truncation away from zero: div(-7,3) = -3) 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. % % AUTHOR % ------ % % 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 %------------------------------------------------------------------------ BEGIN IMPORTING floor_div_lems, abs_rews i,k: VAR int n: VAR nat m: VAR posnat j: VAR nonzero_integer x: VAR real div(i,j): integer = sgn(i)*sgn(j)*floor(abs(i)/abs(j)) div_nat: LEMMA div(n,m) = floor(n/m) div_rew: LEMMA div(n,m) = IF n < m THEN 0 ELSE 1 + div(n-m,m) ENDIF div_def: LEMMA div(i,j) = IF i/j >= 0 THEN floor(i/j) ELSE ceiling(i/j) ENDIF div_value: LEMMA IF sgn(i) = sgn(j) THEN i >= k*j AND i < (k+1)*j IMPLIES div(i,j) = k ELSE i > (k-1)*j AND i <= k*j IMPLIES div(i,j) = k ENDIF div_neg: LEMMA div(-i,j) = -div(i,j) div_neg_d: LEMMA div(i,-j) = -div(i,j) % ================== div for special values ============================= div_zero: LEMMA div(0,j) = 0 div_one: LEMMA abs(j) > 1 IMPLIES div(1,j) = 0 div_minus1: LEMMA abs(j) > 1 IMPLIES div(-1, j) = 0 div_eq_arg: LEMMA div(j,j) = 1 div_by_one: LEMMA div(i,1) = i div_eq_0: LEMMA div(i,j) = 0 IMPLIES abs(i) < abs(j) div_lt: LEMMA abs(i) < abs(j) IMPLIES div(i,j) = 0 div_lt_nat: LEMMA n < m IMPLIES div(n,m) = 0 div_is_0: LEMMA div(i,j) = 0 IFF abs(i) < abs(j) div_parity: LEMMA (sgn(i) = sgn(j) AND abs(i) >= abs(j)) IMPLIES div(i,j) > 0 div_parity_neg: LEMMA (sgn(i) /= sgn(j) AND abs(i) >= abs(j)) IMPLIES div(i,j) < 0 div_ge_0: LEMMA (sgn(i) = sgn(j) IMPLIES div(i,j) >= 0) AND (div(i,j) >= 0 IMPLIES abs(i) < abs(j) OR sgn(i) = sgn(j)) div_le_0: LEMMA (sgn(i) /= sgn(j) IMPLIES div(i,j) <= 0) AND (div(i,j) <= 0 IMPLIES abs(i) < abs(j) OR sgn(i) /= sgn(j)) div_smaller: LEMMA m * div(n,m) <= n div_abs: LEMMA abs(div(i,j)) = div(abs(i),abs(j)) div_max: LEMMA abs(j)*abs(div(i,j)) <= abs(i) % ================== div over addition ================================= div_multiple: LEMMA div(k*j,j) = k div_even: LEMMA integer_pred(i/j) IMPLIES i - j*div(i,j) = 0 div_sum: LEMMA IF integer_pred(i/j) OR sgn(i+k*j) = sgn(i) THEN div(i+k*j,j) = div(i,j) + k ELSE div(i+k*j,j) = div(i,j) + k + sgn(i)*sgn(j) ENDIF b: VAR nat div_sum_nat: LEMMA div(n+b*m,m) = div(n,m) + b nonposint: TYPE = {i: int | i <= 0} CONTAINING -1 negint: TYPE = {i: int | i < 0} CONTAINING -1 npi: VAR nonposint negi: VAR negint JUDGEMENT div(n,m) HAS_TYPE nat JUDGEMENT div(npi,m) HAS_TYPE nonposint JUDGEMENT div(npi,negi) HAS_TYPE nat JUDGEMENT div(m,negi) HAS_TYPE nonposint div_0: LEMMA div(0,j) = 0 AUTO_REWRITE+ div_0 AUTO_REWRITE+ div_eq_arg % LEMMA div(j,j) = 1 AUTO_REWRITE+ div_by_one % LEMMA div(i,1) = i AUTO_REWRITE+ div_multiple % LEMMA div(k*j,j) = k AUTO_REWRITE+ div_lt_nat % LEMMA n < m IMPLIES div(n,m) = 0 AUTO_REWRITE+ div_nat % LEMMA div(n,m) = floor(n/m) END div ¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28