Quelle  symbols_as_interval.pvs

symbols_as_interval : THEORY
BEGIN

  IMPORTING interval

  x,y : VAR real
  X,Y : VAR Interval
  n   : VAR nat

  ;<(X,x) : MACRO bool =
    Lt(X,x)

  ;<=(X,x) : MACRO bool =
    Le(X,x)

  ;>(X,x) : MACRO bool =
    Gt(X,x)

  ;>=(X,x) : MACRO bool =
    Ge(X,x)

  ;+(X,Y) : MACRO Interval =
    Add(X,Y)    

  ;+(x,Y) : MACRO Interval =
    Add([|x|],Y)

  ;+(X,y) : MACRO Interval =
    Add(X,[|y|])

  ;-(X,Y) : MACRO Interval =
    Sub(X,Y)

  ;-(x,Y) : MACRO Interval =
   [|x|]-Y

  ;-(X,y) : MACRO Interval =
   X-[|y|]

  ;-(X) : MACRO Interval =
    Neg(X)

  ;*(X,Y) : MACRO Interval = 
    Mult(X,Y)

  ;*(x,Y) : MACRO Interval =
    [|x|]*Y

  ;*(X,y) : MACRO Interval =
    X*[|y|]

  ;/(X,Y) : MACRO Interval =
    Div(X,Y)

  ;/(x,Y) : MACRO Interval =
    [|x|]/Y

  ;/(X,y) : MACRO Interval =
    X/[|y|]

  ;^(X,n) : MACRO Interval = 
    Pow(X,n)

END symbols_as_interval