Quelle RealInt.pvs Sprache: 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

quality98%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

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.