Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: safe_arith.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.19 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.