Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMSL/MAASL/   (Wiener Entwicklungsmethode ©)  Datei vom 13.4.2020 mit Größe 1 kB image not shown  

SSL min_max.pvs   Interaktion und
PortierbarkeitPVS

 
% A few lemmas about min and max 
min_max : THEORY
BEGIN

  nnx   : VAR nnreal
  npx   : VAR npreal
  x,y,z : VAR real
  px    : VAR posreal

  min_id : LEMMA
    min(x,x) = x

  max_id : LEMMA
    max(x,x) = x

  min_comm : LEMMA
    min(x,y) = min(y,x)

  max_nnreal_0 : LEMMA
    FORALL(x:nnreal): max(x,0) = x

  max_0_nnreal : LEMMA
    FORALL(x:nnreal): max(0,x) = x

  min_nnreal_0 : LEMMA
    FORALL(x:nnreal): min(x,0) = 0

  min_0_nnreal : LEMMA
    FORALL(x:nnreal): min(0,x) = 0

  min_npreal_0 : LEMMA
    FORALL(x:npreal): min(x,0) = x

  min_0_npreal : LEMMA
    FORALL(x:npreal): min(0,x) = x

  max_npreal_0 : LEMMA
    FORALL(x:npreal): max(x,0) = 0

  max_0_npreal : LEMMA
    FORALL(x:npreal): max(0,x) = 0

  max_comm : LEMMA
    max(x,y) = max(y,x)

  min_assoc : LEMMA
    min(min(x,y),z) = min(x,min(y,z))

  max_assoc : LEMMA
    max(max(x,y),z) = max(x,max(y,z))
    
  min_max_id : LEMMA
    min(x,y)+max(x,y) = x+y

  min_max : LEMMA
    min(x,y) = -max(-x,-y)

  max_min : LEMMA
    max(x,y) = -min(-x,-y)

  add_min : LEMMA
    z+min(x,y) = min(z+x,z+y)

  min_sub : LEMMA
    min(x,y)-z = min(x-z,y-z)

  sub_min : LEMMA
    z-min(x,y) = max(z-x,z-y)

  add_max : LEMMA
    z+max(x,y) = max(z+x,z+y)

  max_sub : LEMMA
    max(x,y)-z = max(x-z,y-z)

  sub_max : LEMMA
    z-max(x,y) = min(z-x,z-y)

  abs_max : LEMMA
    abs(x) = max(x,-x)

  abs_min : LEMMA
    abs(x) = -min(x,-x)

  max_abs : LEMMA
    max(x,y) = (x+y+abs(x-y))/2

  nneg_mult_min : LEMMA
    nnx*min(y,z) = min(nnx*y,nnx*z) 

  npos_mult_min : LEMMA
    npx*min(y,z) = max(npx*y,npx*z)

  nneg_mult_max : LEMMA
    nnx*max(y,z) = max(nnx*y,nnx*z) 

  npos_mult_max : LEMMA
    npx*max(y,z) = min(npx*y,npx*z)

  min_div_pos : LEMMA
    min(y,z)/px = min(y/px,z/px) 

  max_div_pos : LEMMA
    max(y,z)/px = max(y/px,z/px) 

  min_le_max_left : LEMMA
    min(max(x,y),z) <= max(min(x,y),z)

  min_le_max_right : LEMMA
    min(max(x,y),z) <= max(x,min(y,z))

  max_rec(F:[nat->real],j:nat,(k:nat|j<=k)): RECURSIVE {r:real|
    (EXISTS (i:nat): j<=i AND i<=k AND F(i)=r) AND
    (FORALL (i:nat): j<=i AND i<=k IMPLIES F(i)<=r)} =
    IF k = j THEN F(j) ELSE
    max(F(k),max_rec(F,j,k-1)) ENDIF
    MEASURE k

  min_rec(F:[nat->real],j:nat,(k:nat|j<=k)): RECURSIVE {r:real|
    (EXISTS (i:nat): j<=i AND i<=k AND F(i)=r) AND
    (FORALL (i:nat): j<=i AND i<=k IMPLIES F(i)>=r)} =
    IF k = j THEN F(j) ELSE
    min(F(k),min_rec(F,j,k-1)) ENDIF
    MEASURE k

  AUTO_REWRITE+ min_id
  AUTO_REWRITE+ max_id
  AUTO_REWRITE+ max_nnreal_0
  AUTO_REWRITE+ max_0_nnreal
  AUTO_REWRITE+ min_nnreal_0
  AUTO_REWRITE+ min_0_nnreal
  AUTO_REWRITE+ min_npreal_0
  AUTO_REWRITE+ min_0_npreal
  AUTO_REWRITE+ max_npreal_0
  AUTO_REWRITE+ max_0_npreal


END min_max

68%


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

*Eine klare Vorstellung vom Zielzustand




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.