Quellcode-Bibliothek safe_arith.pvs Sprache: PVS

safe_arith : THEORY
BEGIN

%
% The comparison interval operators defined in this theory return false when the interval
% operand is empty. The arithmetic interval operators defined in this theory return an empty
% interval when one of the operands is empty (or in the case of division a non-zero divisor).
%
% The theory symbols_as_safe defines the symbols <,<=,>,>=,+,-,*,/,^ using the functions in this theory
%

  IMPORTING interval

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

  safe_Lt(X,x) : bool =
    Proper?(X) AND Lt(X,x)

  safe_Le(X,x) : bool =
    Proper?(X) AND Le(X,x)

  safe_Gt(X,x) : bool =
    Proper?(X) AND Gt(X,x)

  safe_Ge(X,x) : bool =
    Proper?(X) AND Ge(X,x)

  op1 : VAR [Interval->Interval]
  pre : VAR PRED[Interval]
  op2 : VAR [Interval,Interval->Interval]

  Safe1(op1)(X) : Interval =
    IF Proper?(X) THEN op1(X)
    ELSE EmptyInterval
    ENDIF

  Proper_Safe1 : LEMMA
    Proper?(Safe1(op1)(X)) IMPLIES
      Proper?(X) AND
      Safe1(op1)(X) = op1(X)

  Safe1(pre,op1)(X) : Interval =
    IF pre(X) THEN Safe1(op1)(X)
    ELSE EmptyInterval
    ENDIF

  Proper_Safe1_pre : LEMMA
    Proper?(Safe1(pre,op1)(X)) IMPLIES
      pre(X) AND Proper?(X) AND
      Safe1(pre,op1)(X) = op1(X)

  Safe2(op2)(X,Y): Interval =
    IF Proper?(X) AND Proper?(Y) THEN op2(X,Y)
    ELSE EmptyInterval
    ENDIF

  Proper_Safe2 : LEMMA
    Proper?(Safe2(op2)(X,Y)) IMPLIES
      Proper?(X) AND Proper?(Y) AND
      Safe2(op2)(X,Y) = op2(X,Y)

  safe_Add :  [Interval,Interval->Interval] = Safe2(Add)

  safe_Sub :  [Interval,Interval->Interval] = Safe2(Sub)

  safe_Neg :  [Interval->Interval] = Safe1(Neg)

  safe_Abs:  [Interval->Interval] = Safe1(Abs)

  safe_Mult:  [Interval,Interval->Interval] = Safe2(Mult)

  safe_Sq: [Interval->Interval] = Safe1(Sq)

  safe_Pow(X,n) : Interval =
    IF Proper?(X) THEN Pow(X,n)
    ELSE EmptyInterval
    ENDIF

  safe_Div(X,Y) : Interval =
    IF Zeroless?(Y) THEN Safe2(Div)(X,Y)
    ELSE EmptyInterval
    ENDIF

END safe_arith

quality95%

¤ 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.0.19Bemerkung: (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.