Entity:
Real 138 105
null  * 


Operation:
subrange
Real
Sequence(double)
l double step double u double 
 query static
step > 0 & u > l
result = Integer.subrange(0,( ( u - l ) / step )->floor())->collect( x | l + x * step )




Entity:
MathLib 417 61
null  * 
ix int 3 false false true iy int 3 false false true iz int 3 false false true

Operation:
pi
MathLib
double

 query static
true
result = 3.14159265


Operation:
setSeeds
MathLib
void
x int y int z int 
 static
true
ix = x & iy = y & iz = z


Operation:
nrandom
MathLib
double

 query static
true
ix = ( ix@pre * 171 ) mod 30269 & iy = ( iy@pre * 172 ) mod 30307 & iz = ( iz@pre * 170 ) mod 30323 & result = ( ix / 30269.0 + iy / 30307.0 + iz / 30323.0 )


Operation:
random
MathLib
double

 query static
true
r = MathLib.nrandom() & result = ( r - r.floor )


Operation:
combinatorial
MathLib
int
n int m int 
 query static
n >= m & m >= 0
( n - m < m => result = Integer.Prd(m + 1,n,i,i) / Integer.Prd(1,n - m,j,j) ) & ( n - m >= m => result = Integer.Prd(n - m + 1,n,i,i) / Integer.Prd(1,m,j,j) )


Operation:
factorial
MathLib
int
x int 
 query static
true
( x < 2 => result = 1 ) & ( x >= 2 => result = Integer.Prd(2,x,i,i) )


Operation:
gcd
MathLib
int
x int y int 
 query static
x >= 1 & y >= 1
true


Operation:
lcm
MathLib
int
x int y int 
 query static
x >= 1 & y >= 1
result = ( x * y ) / MathLib.gcd(x,y)


Operation:
integrate
MathLib
double
f Sequence(double) d double 
 query static
f.size >= 1 & d >= 1
result = d * f.subrange(2,f.size - 1)->sum() + d * ( f[1] + f.last ) / 2.0






Entity:
NormalDist 238 195
null  * 


Operation:
normal
NormalDist
double
m double sigma double x double 
 query static
true
disp = x - m & denom = ( -0.5 * disp * disp / ( sigma * sigma ) )->exp() & num = sigma * ( 2 * MathLib.pi() )->sqrt() & result = denom / num


Operation:
cumulative
NormalDist
double
m double sigma double x double 
 query static
x >= m
k = ( 1 / ( 1 + 0.2316419 * ( x - m ) ) ) & poly = ( 0.31938153 * k ) + ( -0.356563782 * k * k ) + ( 1.781477937 * k * k * k ) + ( -1.821255978 * k * k * k * k ) + ( 1.330274429 * k * k * k * k * k ) & result = 1 - NormalDist.normal(m,sigma,x) * poly


Operation:
cumulative
NormalDist
double
x double 
 query static
true
( x >= 0 => result = NormalDist.cumulative(0,1,x) ) & ( x < 0 => result = 1 - NormalDist.cumulative(0,1,-x) )


Operation:
sample
NormalDist
double

 query static
true
r1 = MathLib.nrandom() & r2 = MathLib.nrandom() & r3 = MathLib.nrandom() & r4 = MathLib.nrandom() & result = ( r1 + r2 + r3 + r4 ) - 6





Entity:
FinLib 138 55
null  * 


Operation:
euCallOptionPrice
FinLib
double
sharep double strikep double rate double dt double vol double yield double 
 query static
dt > 0
s = sharep - yield & d1 = ( ( s / strikep )->log() + ( rate + vol * vol / 2 ) * dt ) / ( vol * dt.sqrt ) & d2 = d1 - vol * dt.sqrt & result = s * NormalDist.cumulative(d1) - NormalDist.cumulative(d2) * strikep * ( -rate * dt )->exp()


Operation:
euPutOptionPrice
FinLib
double
sharep double strikep double rate double dt double vol double yield double 
 query static
dt > 0
s = sharep - yield & d1 = ( ( s / strikep )->log() + ( rate + vol * vol / 2 ) * dt ) / ( vol * dt.sqrt ) & d2 = d1 - vol * dt.sqrt & result = NormalDist.cumulative(-d2) * strikep * ( -rate * dt )->exp() - s * NormalDist.cumulative(-d1)


Activity:
MathLib gcd
l : int ; k : int ; l := x  ; k := y  ;  while l /= 0 & k /= 0 do if l < k then k := k mod l  else l := l mod k    ; if l = 0 then return k else return l  ; return result      





GeneralUseCase:
testdist 



false


Constraint:
null
true
FinLib.euPutOptionPrice(120,115,0.05,1.5,0.1,10)->display()
null testdist
false



Constraint:
null
true
FinLib.euPutOptionPrice(100,120,0.05,1.5,0.2,5.0)->display()
null testdist
false



Constraint:
null
true
FinLib.euPutOptionPrice(102,95,0.05,1.5,0.4,4)->display()
null testdist
false



Constraint:
null
true
FinLib.euPutOptionPrice(163,170,0.05,1.5,0.25,11.0)->display()
null testdist
false







GeneralUseCase:
testputs 


price Sequence(double) strike Sequence(double) rate double dt double vol Sequence(double) yield Sequence(double) 
false


Constraint:
null
true
Testputs.price = Sequence{120.0,100.0,102.0,163.0} & Testputs.strike = Sequence{115.0,120.0,95.0,170.0} & Testputs.rate = 0.05 & Testputs.dt = 1.5 & Testputs.vol = Sequence{0.1,0.2,0.4,0.25} & Testputs.yield = Sequence{10.0,5.0,4.0,11.0}
null testputs
false



Constraint:
null
true
Integer.subrange(1,4)->forAll( i | FinLib.euPutOptionPrice(Testputs.price->at(i), Testputs.strike->at(i), Testputs.rate, Testputs.dt, Testputs.vol->at(i), Testputs.yield->at(i))->display() )
null testputs
false