Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: prelude_sets_aux.pvs   Sprache: PVS

Untersuchung PVS©

%------------------------------------------------------------------------------
% Properties of (non-real) number fields
%
%     Author: David Lester, Manchester University & NIA
%
%     Version 1.0            5/27/04   Initial version (DRL)
%
%             Narkawicz 12/2013
%------------------------------------------------------------------------------

number_fields_bis: THEORY

  BEGIN

  w, x, y, z:              VAR number_field
  n0x, n0y, n0z, nzx, nzy: VAR nznum

% We have (from the prelude) the following properties of number_fields:
%
%  commutative_add : POSTULATE x + y = y + x
%  associative_add : POSTULATE x + (y + z) = (x + y) + z
%  identity_add    : POSTULATE x + 0 = x
%  inverse_add     : AXIOM x + -x = 0
%  minus_add       : AXIOM x - y = x + -y
%  commutative_mult: AXIOM x * y = y * x
%  associative_mult: AXIOM x * (y * z) =  (x * y) * z
%  identity_mult   : AXIOM 1 * x = x
%  inverse_mult    : AXIOM n0x * (1/n0x) = 1
%  div_def         : AXIOM y/n0x = y * (1/n0x)
%  distributive    : POSTULATE x * (y + z) = (x * y) + (x * z)

% Because the built-in decision procedures only work for reals, we'll restate
% some of the above in order to define AUTO-REWRITEs. Because we don't expect
% users to have to type the names, we'll make the names long so as to avoid
% overloading and potential conflicts.

  number_fields_left_identity_add      : LEMMA 0 + x = x
  number_fields_right_identity_add     : LEMMA x + 0 = x
  number_fields_left_identity_mult     : LEMMA 1 * x = x
  number_fields_right_identity_mult    : LEMMA x * 1 = x
  number_fields_negate_is_left_inverse : LEMMA -x + x = 0
  number_fields_negate_is_right_inverse: LEMMA x + -x = 0

% However, the following are not available unless the field is a subtype
% of real. So we have to add them, proving from the AXIOMs above.

  % Cancellation Laws for equality

  both_sides_plus1:  LEMMA (x + z = y + z) IFF x = y
  both_sides_plus2:  LEMMA (z + x = z + y) IFF x = y
  both_sides_minus1: LEMMA (x - z = y - z) IFF x = y
  both_sides_minus2: LEMMA (z - x = z - y) IFF x = y

  number_fields_negate_negate          : LEMMA -(-x) = x

  zero_times1: LEMMA 0 * x = 0
  zero_times2: LEMMA x * 0 = 0
  nznum_times_nznum_is_nznum: JUDGEMENT *(nzx, nzy) HAS_TYPE nznum
  minus_nznum_is_nznum:       JUDGEMENT -(nzx)      HAS_TYPE nznum
  zero_times3: LEMMA x * y = 0 IFF x = 0 OR y = 0
  neg_times_neg: LEMMA (-x) * (-y) = x * y
  zero_is_neg_zero: LEMMA -0 = 0

  both_sides_times1: LEMMA (x * n0z = y * n0z) IFF x = y
  both_sides_times2: LEMMA (n0z * x = n0z * y) IFF x = y

  inv_ne_0: LEMMA 1/n0x /= 0
  nznum_div_nznum_is_nznum:   JUDGEMENT /(nzx, nzy) HAS_TYPE nznum
  both_sides_div1: LEMMA (x/n0z = y/n0z) IFF x = y
  both_sides_div2: LEMMA (n0z/n0x = n0z/n0y) IFF n0x = n0y

  times_plus: LEMMA (x + y) * (z + w) = x*z + x*w + y*z + y*w
  times_div1: LEMMA x * (y/n0z) = (x * y)/n0z
  times_div2: LEMMA (x/n0z) * y = (x * y)/n0z
  div_eq_zero: LEMMA x/n0z = 0 IFF x = 0

  div_simp:    LEMMA n0x/n0x = 1
  div_cancel1: LEMMA n0z * (x/n0z) = x
  div_cancel2: LEMMA (x/n0z) * n0z = x
  div_cancel3: LEMMA x/n0z = y IFF x = y * n0z
  div_cancel4: LEMMA y = x/n0z IFF y * n0z = x

  cross_mult: LEMMA (x/n0x = y/n0y) IFF (x * n0y = y * n0x)
  div_times:  LEMMA (x/n0x) * (y/n0y) = (x*y)/(n0x*n0y)
  add_div:    LEMMA (x/n0x) + (y/n0y) = (x * n0y + y * n0x)/(n0x * n0y)
  minus_div1: LEMMA (x/n0x) - (y/n0y) = (x * n0y - y * n0x)/(n0x * n0y)
  minus_div2: LEMMA (x/n0x - y/n0x) = (x - y)/n0x
  div_distributes: LEMMA (x/n0z) + (y/n0z) =  (x + y)/n0z
  div_distributes_minus: LEMMA (x/n0z) - (y/n0z) =  (x - y)/n0z
  div_div1:   LEMMA (x / (n0y / n0z)) = ((x * n0z) / n0y)
  div_div2:   LEMMA ((x / n0y) / n0z) = (x / (n0y * n0z))
  idem_add_is_zero: LEMMA x + x = x IMPLIES x = 0

  nonzero_times1: LEMMA n0x * y = 0 IFF y = 0
  nonzero_times2: LEMMA x * n0y = 0 IFF x = 0
  nonzero_times3: LEMMA n0x * n0y = 0 IFF FALSE

  idem_mult: LEMMA x * x = x IFF x = 0 OR x = 1

  number_fields_negative_times         : LEMMA (-x) * y = -(x * y)
  number_fields_times_negative         : LEMMA x * (-y) = -(x * y)

  number_fields_neg1_times        : LEMMA -1*x = -x

%  AUTO_REWRITE+  number_fields_left_identity_add
%  AUTO_REWRITE+  number_fields_right_identity_add
%  AUTO_REWRITE+  number_fields_left_identity_mult
%  AUTO_REWRITE+  number_fields_right_identity_mult
%  AUTO_REWRITE+  number_fields_negate_is_left_inverse
%  AUTO_REWRITE+  number_fields_negate_is_right_inverse
%  AUTO_REWRITE+  number_fields_negate_negate

%  AUTO_REWRITE+  number_fields_bis.zero_times1
%  AUTO_REWRITE+  number_fields_bis.zero_times2
%  AUTO_REWRITE+  number_fields_bis.zero_is_neg_zero

%  AUTO_REWRITE+  number_fields_bis.neg_times_neg
%  AUTO_REWRITE+  number_fields_bis.times_div1
%  AUTO_REWRITE+  number_fields_bis.times_div2

  END number_fields_bis

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.20Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤





Begriffe der Konzeptbildung
Was zu einem Entwurf gehört
Begriffe der Konzeptbildung
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik