Quelle  symbols_as_safe.pvs

symbols_as_safe : THEORY
BEGIN

  IMPORTING safe_arith

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

END symbols_as_safe