Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: RealInt.pvs Sprache: PVS

Original von: PVS^©

%%% Real Intervals %%%
RealInt : THEORY
BEGIN

  RealInt : TYPE = [# lb: real,
               ub: real,
       bounded_below: bool,
       bounded_above: bool,
       closed_below: bool,
       closed_above: bool #]

  I   : VAR RealInt
  x,y : VAR real

  contains?(I)(x): bool =
    (I`bounded_below IMPLIES
      (IF I`closed_below THEN I`lb<=x ELSE I`lb<x ENDIF)) AND
    (I`bounded_above IMPLIES
      (IF I`closed_above THEN x<=I`ub ELSE x<I`ub ENDIF))

  mk_realint(x,y:real,bb,ba,cb,ca:bool) : MACRO RealInt =
    (# lb:=x,ub:=y,bounded_below:=bb,bounded_above:=ba,closed_below:=cb,closed_above:=ca #)

  ;##(x,I) : bool = contains?(I)(x)

  RealInf : DATATYPE WITH SUBTYPES Inf,nInf,RealN
  BEGIN
    oo  : inf? : Inf
    ninf(get_inf:Inf) : ninf? : nInf
    open(get_real:real) : open? : RealN
  END RealInf

  rx,ry : VAR RealInf

  ;-(i:Inf) : nInf = ninf(oo)

  ;[||](x,ry) : RealInt =
    LET y = IF open?(ry) THEN get_real(ry) ELSIF ninf?(ry) THEN x-1 ELSE x+1 ENDIF IN
    mk_realint(x,y,TRUE,open?(ry),TRUE,FALSE)

  ;[||](rx,y) : RealInt =
    LET x = IF open?(rx) THEN get_real(rx) ELSIF inf?(rx) THEN y+1 ELSE y-1 ENDIF IN
    mk_realint(x,y,open?(rx),TRUE,FALSE,TRUE)

  ;[||](rx,ry) : RealInt =
    LET x = IF open?(rx) THEN get_real(rx)
            ELSIF open?(ry) THEN
              IF inf?(rx) THEN get_real(ry)+1
              ELSE get_real(ry)-1
              ENDIF
            ELSE -1 ENDIF,
        y = IF open?(ry) THEN get_real(ry)
            ELSIF open?(rx) THEN
              IF ninf?(ry) THEN get_real(rx)-1
              ELSE get_real(rx)+1
              ENDIF
            ELSE 1 ENDIF IN
    mk_realint(x,y,open?(rx),open?(ry),FALSE,FALSE)

  z : VAR real

  in_ninf_inf : LEMMA
    z ## [| -oo, oo |]

  in_ninf_open : LEMMA
    z ## [| -oo, open(y) |] IFF z < y

  in_open_inf : LEMMA
    z ## [| open(x), oo |] IFF z > x

  in_open_open : LEMMA
    z ## [| open(x), open(y) |] IFF x < z AND z < y

  in_ninf_close : LEMMA
    z ## [| -oo, y |] IFF z <= y

  in_close_inf : LEMMA
    z ## [| x, oo |] IFF z >= x

END RealInt

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.