|
proper_arith : THEORY
BEGIN
%
% The comparison and arithmetic operators defined in this theory require operands to be non-empty
% (and in the case of division a non-zero divisor). The PVS's type-checker will generate TCCs that enforces
% these properties.
%
% The theory symbols_as_proper defines the symbols +,-,*,/,^ using the functions in this theory
%
IMPORTING interval
x,y : VAR real
X,Y : VAR ProperInterval
n : VAR nat
NzInterval : TYPE = { X | Zeroless?(X) }
PosInterval : TYPE = { X | Pos?(X) }
NegInterval : TYPE = { X | Neg?(X) }
NonNegInterval : TYPE = { X | NonNeg?(X) }
proper_Lt(X,x) : bool =
Lt(X,x)
proper_Le(X,x) : bool =
Le(X,x)
proper_Gt(X,x) : bool =
Gt(X,x)
proper_Ge(X,x) : bool =
Ge(X,x)
proper_Add(X,Y) : ProperInterval =
Add(X,Y)
proper_Sub(X,Y) : ProperInterval =
Sub(X,Y)
proper_Neg(X) : ProperInterval =
Neg(X)
proper_Mult(X,Y) : ProperInterval =
Mult(X,Y)
YNz : VAR NzInterval
ynz : VAR nzreal
proper_Div(X,YNz) : ProperInterval =
Div(X,YNz)
proper_Pow(X,n) : ProperInterval =
Pow(X,n)
proper_Abs(X) : ProperInterval =
Abs(X)
proper_Sq(X) : ProperInterval =
Sq(X)
END proper_arith
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
