Overture Tool
Formal Modelling in VDM
newspeakSL
Author: Paul Mukherjee
The programming language NewSpeak? is a language designed specifically for use in safety-critical systems. It employs the notion of Orwellian programming - undesirable properties are avoided by restricting the syntax of the programming language. This is a formal semantics for the language in VDM-SL. Details of the language and its semantics:
P. Mukherjee, “A Semantics for NewSpeak? in VDM-SL”. In T. Denvir, M. Naftalin, M. Bertran (eds), “FME ‘94: Industrial Benefit of Formal Methods”, Springer-Verlag, October 1994.
I.F. Currie, “NewSpeak - a reliable programming language”. In C. Sennett (ed), “High-Integrity Software”, Pitman 1989.
| Properties | Values |
|---|---|
| Language Version: | vdm10 |
| Entry point : | DEFAULT`max({3,1,5,8,3,2,5,4,22}) |
newspeak.vdmsl
values
beta:nat1 = 2;
epsilon_r:real = 1;
epsilon_t:real = 1;
bytemax:int = 10000;
maxint:int = 100000;
Phi: Fl_elt = mk_Fl_elt(<phi>,1);
zerot:Time = mk_(0,0);
t_absreal:Time = mk_(1,1);
t_absint:Time = mk_(1,1);
t_realmonminus:Time = mk_(1,1);
t_intmonminus:Time = mk_(1,1);
t_not:Time = mk_(1,1);
t_discard:Time = mk_(1,1);
t_round:Time = mk_(1,1);
t_mantissa:Time = mk_(1,1);
t_exponent:Time = mk_(1,1);
t_odd:Time = mk_(1,1);
t_float:Time = mk_(1,1);
t_min:Time = mk_(1,1);
t_max:Time = mk_(1,1);
t_intbinop:Time = mk_(1,1);
t_realbinop:Time = mk_(1,1);
t_intcomp:Time = mk_(1,1);
t_realcomp:Time = mk_(1,1);
t_tr_eq:Time = mk_(1,1);
t_real_eq:Time = mk_(1,1);
t_int_eq:Time = mk_(1,1);
t_void_eq:Time = mk_(1,1);
t_and:Time = mk_(1,1);
t_skip:Time = mk_(1,1);
t_access:Time = mk_(1,1);
t_comp_extract:Time = mk_(1,1);
t_update:Time = mk_(1,1);
t_construct_ev:Time = mk_(1,1);
t_const_type:Time = mk_(1,1);
t_widen_type:Time = mk_(1,1);
t_if: Time = mk_(1,1)
types
Errvalue = <err>;
Id = token;
Flavdom = set of Fl_elt;
Fl_elt::label : token | <phi>
dim : rat;
Tr:: val: bool
type: TrType;
TrType:: range: set of bool
fl: Flavdom;
EqOp = <EQ> | <NEQ>;
Int::val : int
type : IntType;
IntType:: rep : <byte> | <word>
range : set of int
fl : Flavdom;
NumOp :: <numplus> | <binaryminus> | <nummult> | <numdiv> | <nummod>
| <nummax> | <nummin>;
CompOp = <numgt> | <numlt> | <numge> | <numle>;
Real::val:real
type:Float;
Floatrng::lower:int
upper:int;
Float::range:set of Floatrng
abserr: real
relerr: real
fl:Flavdom;
Void::val:<nil>
type: VoidType;
VoidType :: fl: Flavdom;
Structure:: val: StructValue
type: StructureType;
StructValue = seq1 of Component;
Component = int | real | bool;
StructureType :: tps: seq1 of CompType
fl : Flavdom;
CompType = TrType | Float | IntType;
Vector::val: VectorValue
type: VectorType;
VectorValue = seq1 of Tr | seq1 of Real | seq1 of Int | seq1 of Void |
seq1 of Errvalue | seq1 of VectorValue | seq1 of StructValue;
VectorType :: lower: int
upper: int
type : Expressible_type
fl : Flavdom;
Union:: val : UnionValue
type : UnionType;
UnionValue = Int | Real | Tr | Void;
UnionType :: tps : set of (IntType | Float | TrType | VoidType)
fl : Flavdom;
Expressible_type = TrType | Float | IntType | VoidType | VectorType |
StructureType | UnionType;
Location :: nat;
Expressible_value = Errvalue | Tr | Int | Real | Void | Structure |
Union | Vector;
Storable_value :: Tr | Real | Int | Void | Vector | Structure | Union;
Store = map Location to Storable_value;
Time = nat * nat;
PState:: sto : Store
time : Time;
Denotable_value = Location | Storable_value | Errvalue |
Expressible_type | Proc;
Env = (map Id to Denotable_value) * Location;
EnvState = (Env * PState) | Errvalue;
EST_value:: val : Expressible_value
sto : Store
time : Time;
EST_Iterate :: expst : EST_value
i : int;
Param = seq of Expressible_value;
Proc :: Param -> PState -> EST_value;
Formal_elt :: id : Id
rep : Expressible_type
fl : Flavdom;
Program :: Expression;
Expression :: Operation | InnerLoop | Assignment | Scope |
GuardedScope | Assertion | TimedExpression;
Operation :: MonOperation | BinaryOperation;
MonOperation :: MonOpMonOperand | VectorOperation | Value;
MonOpMonOperand :: operator : MonOp
operand : MonOperation;
MonOp = <numabs> | <unaryminus> | <not> | CompileTimeOp | <odd> |
<round> | <float> | <mantissa> | <exponent> | <discard>;
CompileTimeOp :: <inf> | <sup> | <relonly> | <absonly> | <relerr> |
<abserr>;
VectorOperation :: vo : VectorOp
mo : MonOperation
mult : [Multiple];
VectorOp = <sum> | <product> | <all> | <some> | <vecmax> | <vecmin> |
<flatten>;
Multiple :: op : Operation
to_p : ToPart;
ToPart = Upto | Downto;
Upto = Operation;
Downto = Operation;
BinaryOperation:: left : MonOperation
opr : BinaryOp
right : MonOperation;
BinaryOp :: NumOp | CompOp | EqOp | BoolOp | VecBinOp | <replaceflav>;
BoolOp = <and> | <or>;
VecBinOp = <concat>;
Value :: ConstantValue | NamedValue | VectorVal | Sequence | Call |
StructureValue | Widening | Conditional | OuterLoop;
ConstantValue :: IntegerDenotation | FloatingDenotation | Ascii_Char |
BooleanDenotation | Ascii_string | Flavouring |
<skip>;
IntegerDenotation :: int;
FloatingDenotation :: real;
BooleanDenotation :: bool;
Ascii_Char :: char;
Ascii_string :: seq1 of char;
NamedValue :: Id | FlavourExtract | FlavourStrip | VectorExtract |
VectorTrimming;
FlavourExtract :: nv : NamedValue
fl : Flavouring;
Flavouring :: seq of Flavour;
Flavour:: name : token
index : [rat];
FlavourStrip :: nv:NamedValue
fl : Flavouring;
VectorExtract :: named : NamedValue
index : Operation;
VectorTrimming :: named : NamedValue
to_p : <gtvalue> | <ltvalue> | <atvalue>
ctv : CompileTimeValue;
CompileTimeValue :: Operation;
VectorVal :: seq1 of Operation;
Sequence :: seq1 of Expression;
Call :: id : Id
acts: seq of Operation;
StructureValue :: seq1 of Operation;
Widening :: expr : Expression
tp : Type;
Type :: PrimitiveType | StrucType | VecType | FlavouredType | UnionTp |
TypeName;
PrimitiveType :: Number | FloatType | VoidValType;
Number :: rep : <bit> | <byte> | <word>
range : seq of Range;
Range::lower : [CompileTimeValue]
upper : [CompileTimeValue];
FloatType :: range : seq of Range
abserr : [CompileTimeValue]
relerr : [CompileTimeValue];
VoidValType = Flavouring;
VecType :: range : Range
tp : Type;
StrucType :: seq1 of Type;
FlavouredType::fl : Flavouring
tp : Type;
UnionTp :: seq1 of Type;
TypeName :: Id;
Conditional :: IfThenOnly | IfThenElse | CaseExpr;
IfThenOnly :: prop : Expression
action : Sequence;
IfThenElse :: prop : Expression
thenaction : Sequence
elseaction : Sequence;
CaseExpr :: expr : Expression
limbs : seq1 of CaseLimb
out : [Outlimb];
CaseLimb :: test : Tester
sequ : Sequence;
Tester = SkeletonType | StrucTest | NonStrucTest;
SkeletonType :: Type | NumSkel | StrucSkel | FlavSkel | VecSkel |
UnionSkel;
NumSkel :: ranges : [seq1 of Range]
errors: [Errors];
Errors :: abserr : [CompileTimeValue]
relerr : [CompileTimeValue];
StrucSkel :: seq1 of (SkeletonType | <nil>);
FlavSkel:: skel : SkeletonType
fl : Flavouring;
VecSkel :: SkeletonType;
UnionSkel :: seq1 of (FlavouredType | VoidValType | FlavSkel);
StrucTest :: seq1 of (NonStrucTest | <nil>);
NonStrucTest :: id : [Id]
fl : [Flavouring]
tp : SkeletonType;
Outlimb = Sequence;
OuterLoop :: OuterIntLoop | OuterVecLoop;
OuterIntLoop :: ovr : OverRange
actions : Sequence;
OverRange :: cnt : LoopId
range : Range;
LoopId = Id;
OuterVecLoop :: ovs : OverVectors
action : Sequence;
OverVectors :: cnt : [LoopId]
ovv : seq1 of OverVector;
OverVector :: id : Id
val : Operation;
InnerLoop :: IntLoop | VecLoop | TimeLoop;
IntLoop :: inc : InnerControl
actions : Sequence;
InnerControl = OverRange | PartialRange;
PartialRange :: cnt : LoopId
from_p : Operation
to_p : ToPart
inc : [Operation];
VecLoop :: ovs : OverVectors
actions : Sequence;
TimeLoop :: time : TimeInterval
actions : Sequence;
TimeInterval = Range;
Assignment :: NvAssignment | MultAssignment | StrAssignment;
NvAssignment :: dest : Id
expr : Expression;
MultAssignment :: dest : Id
mult : Multiple
expr : Expression;
StrAssignment :: dest : seq1 of Id
expr : Expression;
Scope :: SimpleScope | PackageScope;
SimpleScope :: decls : seq1 of Declaration
expr : Expression;
Declaration = ImportDecl | ExportDecl | LetDecl | VarDecl | ProcDec |
TypeDec;
ImportDecl :: id : Id
tp : Type;
ExportDecl :: id : Id
expr : Expression;
LetDecl :: SimpleLetDecl | StrucLetDecl;
SimpleLetDecl :: id : Id
expr : Expression;
StrucLetDecl :: ids : seq1 of Id
expr : Expression;
VarDecl :: id : Id
expr : Expression;
ProcDec :: nls : [NonLocals]
ph : ProcHeading
expr : Expression;
NonLocals :: ids : [seq1 of Id]
decls : [seq1 of Declaration];
ProcHeading :: id : Id
formals : seq of Formal;
Formal :: id : Id
rep : Representation
fl : Flavouring;
Representation = PrimitiveRep | StrucRep | VecRep| UnionRep |
FlavouredRep | Type;
PrimitiveRep :: NumRep | FloatRep;
NumRep :: rep : <bit> | <byte> | <word>
rnage : [seq1 of Range];
FloatRep :: range : [seq1 of Range]
abserr : [CompileTimeValue]
relerr : [CompileTimeValue];
StrucRep :: seq1 of Representation;
VecRep :: range : Range
rep : Representation;
UnionRep :: seq1 of Representation;
FlavouredRep :: fl :Flavouring
rep : Representation;
TypeDec :: id : Id
tp : Type;
PackageScope :: ids : seq1 of Id
decls : seq1 of Declaration
expr : Expression;
GuardedScope :: decls : seq1 of GuardedDeclaration
inseq : Sequence
out : Sequence;
GuardedDeclaration = Declaration | WhereDecl;
WhereDecl :: type : SkeletonType
expr : Expression
id : [Id];
Assertion :: expr : Expression
tp : SkeletonType;
TimedExpression :: TimeTakes | TimeAssertion;
TimeTakes :: expr : Expression
time : TimeInterval;
TimeAssertion :: expr : Expression
time : TimeInterval
functions
fl_mult: Flavdom * Flavdom -> Flavdom
fl_mult(f1,f2) ==
if Phi in set f1 union f2
then {Phi}
else {mk_Fl_elt(f.label,f.dim + f'.dim) | f in set f1, f' in set f2
& f.label = f'.label} union
{ f | f in set f1 & forall f' in set f2 & f'.label <> f.label} union
{ f | f in set f2 & forall f' in set f1 & f'.label <> f.label};
fl_div: Flavdom * Flavdom -> Flavdom
fl_div(f1,f2) ==
if Phi in set f1 union f2
then {Phi}
else {mk_Fl_elt(f.label,f.dim - f'.dim) | f in set f1, f' in set f2
& f.label = f'.label} union
{ f | f in set f1 & forall f' in set f2 & f'.label <> f.label} union
{ mk_Fl_elt(f.label,-f.dim) |
f in set f2 & forall f' in set f1 & f'.label <> f.label};
phi_remove: Expressible_type -> Expressible_type
phi_remove(tp) ==
cases tp:
mk_VoidType(t) -> mk_VoidType(t\ {Phi}),
mk_TrType(range,fl) -> mk_TrType(range,fl \ {Phi}),
mk_IntType(rep,range,fl) -> mk_IntType(rep,range, fl \ {Phi}),
mk_Float(range,abse,rele,fl) -> mk_Float(range,abse,rele,fl\{Phi}),
mk_VectorType(lower,upper,tp,fl) ->
mk_VectorType(lower,upper,tp, fl\{Phi}),
mk_StructureType(tps,fl) -> mk_StructureType(tps,fl\{Phi}),
mk_UnionType(tps,fl) -> mk_UnionType(tps,fl\{Phi})
end;
tr_eq: Tr * Tr * EqOp -> Expressible_value
tr_eq(t1,t2,op) ==
if t1.type.fl <> t2.type.fl
then <err>
elseif op = <EQ>
then mk_Tr(t1.val = t2.val, mk_TrType({b1 = b2 | b1 in set
t1.type.range, b2 in set t2.type.range},{}))
else mk_Tr(t1.val <> t2.val, mk_TrType({b1 <> b2 | b1 in set
t1.type.range, b2 in set t2.type.range},{}));
tr_and: Tr * Tr -> Expressible_value
tr_and(t1,t2) ==
if t1.type.fl <> t2.type.fl
then <err>
else mk_Tr(t1.val and t2.val,
mk_TrType({b1 and b2 | b1 in set t1.type.range, b2 in set
t2.type.range },t1.type.fl));
tr_or: Tr * Tr -> Expressible_value
tr_or(t1,t2) ==
if t1.type.fl <> t2.type.fl
then <err>
else mk_Tr(t1.val or t2.val,
mk_TrType({b1 or b2 | b1 in set t1.type.range, b2 in set
t2.type.range },t1.type.fl));
tr_not: Tr -> Expressible_value
tr_not(t) ==
mk_Tr(not t.val, mk_TrType({ not b | b in set t.type.range},t.type.fl));
int_eq: Int * Int * EqOp -> Expressible_value
int_eq(z1,z2,op) ==
if z1.type.fl <> z2.type.fl
then <err>
elseif op = <EQ>
then mk_Tr(z1.val = z2.val, mk_TrType({i = j | i in set
z1.type.range, j in set z2.type.range},{}))
else mk_Tr(z1.val <> z2.val, mk_TrType({i <> j | i in set
z1.type.range, j in set z2.type.range},{}));
min: set1 of real -> real
min(s) ==
let m in set s in
if card s = 1 then m
else let sm = min(s\{m}) in
if m < sm then m else sm;
max: set1 of real -> real
max(s) ==
let m in set s in
if card s = 1 then m
else let sm = max(s\{m}) in
if m > sm then m else sm;
intbinop: Int * Int * NumOp -> Expressible_value
intbinop(x,y,mk_NumOp(op)) ==
cases op:
(<numplus>) -> intplus(x,y),
(<binaryminus>) -> intbinminus(x,y),
(<nummult>) -> intmult(x,y),
(<numdiv>) -> intdiv(x,y),
(<nummod>) -> intmod(x,y),
(<nummax>) -> intmax(x,y),
(<nummin>) -> intmin(x,y)
end;
intplus: Int * Int -> Expressible_value
intplus(x,y) ==
if x.type.fl <> y.type.fl
then <err>
else let range = { i + j | i in set x.type.range, j in set
y.type.range} in
if max({abs min(range), abs max(range)}) >= maxint
then <err>
else let rep = if min({abs min(range),abs max(range)}) >= bytemax
or x.type.rep = <word> or y.type.rep = <word>
then <word>
else <byte> in
mk_Int(x.val + y.val, mk_IntType(rep,range,x.type.fl));
intbinminus: Int * Int -> Expressible_value
intbinminus(x,y) ==
if x.type.fl <> y.type.fl
then <err>
else let range = { i - j | i in set x.type.range, j in set
y.type.range} in
if max({abs min(range), abs max(range)}) >= maxint
then <err>
else let rep = if min({abs min(range),abs max(range)}) >= bytemax
or x.type.rep = <word> or y.type.rep = <word>
then <word>
else <byte> in
mk_Int(x.val - y.val, mk_IntType(rep,range,x.type.fl));
intmult: Int * Int -> Expressible_value
intmult(x,y) ==
let fl = fl_mult(x.type.fl,y.type.fl),
range = { i * j | i in set x.type.range, j in set y.type.range} in
if max({abs min(range), abs max(range)}) >= maxint
then <err>
else let rep = if min({abs min(range),abs max(range)}) >= bytemax
or x.type.rep = <word> or y.type.rep = <word>
then <word>
else <byte> in
mk_Int(x.val * y.val, mk_IntType(rep,range,fl));
intdiv: Int * Int -> Expressible_value
intdiv(x,y) ==
if 0 in set y.type.range
then <err>
else let fl = fl_div(x.type.fl,y.type.fl),
range = { i div j | i in set x.type.range, j in set
y.type.range} in
if max({abs min(range), abs max(range)}) >= maxint
then <err>
else let rep = if exists r in set range & abs r >= bytemax
then <word> else <byte> in
mk_Int(x.val div y.val, mk_IntType(rep,range,fl));
intmod: Int * Int -> Expressible_value
intmod(x,y) ==
if 0 in set y.type.range
then <err>
else let range = { i mod j | i in set x.type.range, j in set
y.type.range} in
mk_Int(x.val mod y.val,mk_IntType(y.type.rep,range,x.type.fl));
intmax: Int * Int -> Expressible_value
intmax(x,y) ==
if x.type.fl <> y.type.fl
then <err>
else let rep = if (x.type.rep = <word>) or (y.type.rep = <word>)
then <word> else <byte>,
range = {max({i,j}) | i in set x.type.range, j in set
y.type.range} in
mk_Int(max({x.val,y.val}),mk_IntType(rep,range,x.type.fl));
intmin: Int * Int -> Expressible_value
intmin(x,y) ==
if x.type.fl <> y.type.fl
then <err>
else let rep = if (x.type.rep = <word>) or (y.type.rep = <word>)
then <word> else <byte>,
range = {min({i,j}) | i in set x.type.range, j in set
y.type.range} in
mk_Int(min({x.val,y.val}),mk_IntType(rep,range,x.type.fl));
absint: Int -> Int
absint(z) ==
mk_Int(abs z.val, mk_IntType(z.type.rep, { abs i | i in set
z.type.range}, z.type.fl));
intmonminus: Int -> Int
intmonminus(z) ==
mk_Int(-z.val, mk_IntType(z.type.rep, {-i | i in set z.type.range},
z.type.fl)) ;
odd: Int -> Tr
odd(z) ==
let range = { x mod 2 = 0 | x in set z.type.range} in
mk_Tr(z.val mod 2 = 0, mk_TrType(range,{}));
intcomp: Int * Int * CompOp -> Expressible_value
intcomp(x,y,op) ==
if x.type.fl <> y.type.fl
then <err>
else let p = lambda mk_(i,j): int * int &
cases op:
<numgt> -> i > j,
<numlt> -> i < j,
<numge> -> i >= j,
<numle> -> i <= j
end in
let val = p(mk_(x.val,y.val)),
range = {p(mk_(i,j)) | i in set x.type.range, j in set
y.type.range} in
mk_Tr(val,mk_TrType(range,{}));
ascii : char -> int
ascii(c) == 1;
float: Int -> Real
float(z) ==
mk_Real(z.val,mk_Float({mk_Floatrng(min(z.type.range),max(z.type.range))},
maxint,maxint,{}));
real_eq: Real * Real * EqOp -> Expressible_value
real_eq(r,s,op) ==
if r.type.fl <> s.type.fl
then <err>
else let r1 =
dunion {{floor((1-r.type.relerr) * range.lower -
r.type.abserr),..., floor(0.5 + (1+r.type.relerr) *
range.upper + r.type.abserr)} | range in set r.type.range},
r2 =
dunion {{floor((1-s.type.relerr) * range.lower -
s.type.abserr),..., floor(0.5 + (1+s.type.relerr) *
range.upper + s.type.abserr)} | range in set s.type.range} in
let range = if r1 inter r2 = {} then {false} else {true,false} in
if op = <EQ>
then mk_Tr(r.val = s.val, mk_TrType(range,{}))
else mk_Tr(r.val <> s.val, mk_TrType({ not t | t in set range},{}));
absreal: Real -> Real
absreal(r) ==
let new_range =
{ mk_Floatrng(min({abs range.lower, abs range.upper}),
max({abs range.lower, abs range.upper}))
| range in set r.type.range} in
mk_Real(abs r.val, mu (r.type, range |-> new_range));
realmonminus: Real -> Real
realmonminus(r) ==
mk_Real(-r.val,mu (r.type, range |->
{ mk_Floatrng(- range.upper, -range.lower) | range in set r.type.range}));
realbinop: Real * Real * NumOp -> Expressible_value
realbinop(x,y,mk_NumOp(op)) ==
cases op:
<numplus> -> realplus(x,y),
<binaryminus> -> realbinminus(x,y),
<nummult> -> realmult(x,y),
<numdiv> -> realdiv(x,y),
<nummax> -> realmax(x,y),
others -> <err>
end;
realplus:Real * Real -> Expressible_value
realplus(x,y) ==
if x.type.fl <> y.type.fl
then <err>
else let range = {mk_Floatrng(xrange.lower + yrange.lower,
xrange.upper + yrange.upper) | xrange in set
x.type.range, yrange in set y.type.range},
Xmax = max(dunion {{abs range.lower,abs range.upper} |
range in set x.type.range}),
Ymax = max(dunion {{abs range.lower,abs range.upper} |
range in set y.type.range}),
XYmax = max({Xmax,Ymax}) in
if max({max({abs r.lower, abs r.upper}) | r in set range}) >= maxint
then <err>
else let As = x.type.relerr + y.type.abserr + x.type.relerr *
Xmax + y.type.relerr * Ymax + epsilon_t*XYmax in
let val = x.val + y.val,
type = mk_Float(range,As,epsilon_r,x.type.fl) in
mk_Real(val,type);
realbinminus: Real * Real -> Expressible_value
realbinminus(x,y) ==
if x.type.fl <> y.type.fl
then <err>
else let range = {mk_Floatrng(xrange.lower - yrange.upper,
xrange.upper - yrange.lower) | xrange in set
x.type.range, yrange in set y.type.range},
Xmax = max(dunion {{abs range.lower,abs range.upper} |
range in set x.type.range}),
Ymax = max(dunion {{abs range.lower,abs range.upper} |
range in set y.type.range}),
XYmax = max({Xmax,Ymax}) in
if max({max({abs r.lower, abs r.upper}) | r in set range}) >= maxint
then <err>
else let As = x.type.relerr + y.type.abserr + x.type.relerr *
Xmax + y.type.relerr * Ymax + epsilon_t*XYmax in
let val = x.val - y.val,
type = mk_Float(range,As,epsilon_r,x.type.fl) in
mk_Real(val,type);
realmult: Real * Real -> Expressible_value
realmult(x,y) ==
let range = {mk_Floatrng(xrange.lower * yrange.lower,
xrange.upper * yrange.upper) | xrange in set
x.type.range, yrange in set y.type.range},
Xmax = max(dunion {{abs range.lower,abs range.upper} |
range in set x.type.range}),
Ymax = max(dunion {{abs range.lower,abs range.upper} |
range in set y.type.range}),
XYmax = max({Xmax,Ymax}) in
if max({max({abs r.lower, abs r.upper}) | r in set range})
>= maxint
then <err>
else let As = Xmax * Ymax * (x.type.relerr + y.type.relerr) +
x.type.abserr * Ymax * (1+y.type.relerr) +
y.type.abserr * Xmax * (1+x.type.relerr) +
x.type.abserr * y.type.abserr + epsilon_t *XYmax,
fl = fl_mult(x.type.fl, y.type.fl) in
mk_Real(x.val * y.val, mk_Float(range,As,epsilon_r,fl));
realdiv: Real * Real -> Expressible_value
realdiv(x,y) ==
if (((1-y.type.relerr) * min({range.lower | range in set y.type.range})
- y.type.abserr) <=0 ) and
(((1+y.type.relerr) * max({range.upper | range in set y.type.range})
+ y.type.abserr) >=0 )
then <err>
else let range = {mk_Floatrng(floor (xrange.lower / yrange.upper),
floor(0.5+ xrange.upper / yrange.lower)) |
xrange in set x.type.range,
yrange in set y.type.range},
Xmax = max(dunion {{abs range.lower,abs range.upper} |
range in set x.type.range}),
Ymax = max(dunion {{abs range.lower,abs range.upper} |
range in set y.type.range}),
XYmax = max({Xmax,Ymax}),
Ymin = min(dunion {{abs range.lower,abs range.upper}
| range in set y.type.range}) in
if max({max({abs r.lower, abs r.upper}) | r in set range})
>= maxint
then <err>
else let As = ((Xmax * Ymax * max({x.type.relerr, y.type.relerr}) +
Ymax * x.type.abserr + Xmax * y.type.abserr)
/Ymin ** 2) + epsilon_t * XYmax,
fl = fl_div(x.type.fl,y.type.fl) in
mk_Real(x.val/y.val, mk_Float(range,As,epsilon_r,fl));
realmax: Real * Real -> Expressible_value
realmax(x,y) ==
if x.type.fl <> y.type.fl
then <err>
else let val = max({x.val,y.val}),
abserr = max({x.type.abserr,y.type.abserr}),
relerr = max({x.type.relerr,y.type.relerr}),
range = { mk_Floatrng(max({xr.lower,yr.lower}),
max({xr.upper,yr.upper})) |
xr in set x.type.range,
yr in set y.type.range} in
mk_Real(val,mk_Float(range,abserr,relerr,x.type.fl));
realmin: Real * Real -> Expressible_value
realmin(x,y) ==
if x.type.fl <> y.type.fl
then <err>
else let val = min({x.val,y.val}),
abserr = max({x.type.abserr,y.type.abserr}),
relerr = max({x.type.relerr,y.type.relerr}),
range = { mk_Floatrng(min({xr.lower,yr.lower}),
min({xr.upper,yr.upper})) |
xr in set x.type.range,
yr in set y.type.range} in
mk_Real(val,mk_Float(range,abserr,relerr,x.type.fl));
discard: Real -> Int
discard(r) ==
mk_Int(floor (r.val + 0.5),
mk_IntType(<word>,dunion {{range.lower,...,range.upper} |
range in set r.type.range}, {}));
round: Real -> Int
round(r) ==
if is_int(r.val)
then mk_Int(r.val,mk_IntType(<word>, dunion {{range.lower,...,range.upper} |
range in set r.type.range},{}))
else mk_Int(floor (r.val + 0.5),mk_IntType(<word>,
dunion {{range.lower,...,range.upper} |range in set r.type.range},
{}));
realcomp: Real * Real * CompOp -> Expressible_value
realcomp(x,y,op) ==
if x.type.fl <> y.type.fl
then <err>
else let p = lambda mk_(i,j): real * real &
cases op:
<numgt> -> i > j,
<numlt> -> i < j,
<numle> -> i <= j,
<numge> -> i >= j
end,
xrange = dunion {{(1-x.type.relerr)*range.lower - x.type.abserr,...,
(1+x.type.relerr)*range.upper + x.type.abserr}
| range in set x.type.range},
yrange = dunion {{(1-y.type.relerr)*range.lower - y.type.abserr,...,
(1+y.type.relerr)*range.upper + y.type.abserr}
| range in set y.type.range} in
let val = p(mk_(x.val,y.val)),
range = if max(xrange) < min(yrange)
then {p(mk_(max(xrange),min(yrange)))}
elseif min(xrange) > max(yrange)
then {p(mk_(max(yrange),min(xrange)))}
else {true,false} in
mk_Tr(val,mk_TrType(range,{}));
inf: Real -> Real
inf(r) ==
let m = min({range.lower | range in set r.type.range}) *
(1- r.type.relerr) - r.type.abserr in
mk_Real(m,mk_Float({mk_Floatrng(m,m)},0,0,{Phi}));
sup: Real -> Real
sup(r) ==
let m = max({range.upper | range in set r.type.range}) *
(1+ r.type.relerr) + r.type.abserr in
mk_Real(m,mk_Float({mk_Floatrng(m,m)},0,0,{Phi}));
absonly: Real -> Real
absonly(mk_Real(r,f)) ==
let abse = f.abserr + (r * f.relerr) in
mk_Real(r, mu(f, abserr |-> abse, relerr |-> 0));
relonly: Real -> Real
relonly(mk_Real(r,f)) ==
if r = 0 then mk_Real(r,mu(f,relerr |-> 0, abserr |-> 0))
else let rel = f.relerr + f.abserr/r in
mk_Real(r,mu(f,relerr |-> rel, abserr |-> 0));
abserr: Real -> Real
abserr(r) ==
mk_Real(r.type.abserr,
mk_Float({mk_Floatrng(r.type.abserr,r.type.abserr)}, 0,0,{Phi}));
relerr: Real -> Real
relerr(r) ==
mk_Real(r.type.relerr,
mk_Float({mk_Floatrng(r.type.relerr,r.type.relerr)}, 0,0,{Phi}));
void_eq: Void * Void * EqOp -> Expressible_value
void_eq(v1,v2,op) ==
if (v1.type = v2.type) and op = <EQ>
then mk_Tr(true,mk_TrType({true},{}))
elseif (v1.type <> v2.type) and op = <NEQ>
then mk_Tr(true,mk_TrType({true},{}))
else mk_Tr(false,mk_TrType({false},{}));
construct_ev: Component * CompType -> Expressible_value
construct_ev(v,t) ==
if is_real(v) then mk_Real(v,t)
elseif is_bool(v) then mk_Tr(v,t)
else mk_Int(v,t);
comp_extract: Structure * Flavdom -> Expressible_value
comp_extract(s,fl) ==
let matches = { i | i in set inds s.val & s.type.tps(i).fl = fl} in
if card matches <> 1
then <err>
else let {i} = matches in
construct_ev(s.val(i),s.type.tps(i));
struc_length:StructureType -> nat
struc_length(s) ==
len s.tps;
vector_extract: Vector * int -> Expressible_value
vector_extract(v,i) ==
v.val(i - v.type.lower + 1);
vector_subv: VectorValue * int * int -> VectorValue
vector_subv(v,l,u) ==
v(l,...,u);
vector_length: VectorType -> nat
vector_length(v) ==
v.type.upper - v.type.lower + 1;
vector_flatten:VectorValue -> VectorValue
vector_flatten(vs) ==
conc vs;
vector_sum: VectorValue -> Expressible_value
vector_sum(v) ==
if len v = 1
then hd v
else let s = vector_sum(tl v) in
if s = <err>
then <err>
elseif is_Real(hd v)
then realplus(hd v,s)
else intplus(hd v,s);
vector_product: VectorValue -> Expressible_value
vector_product(v) ==
if len v = 1
then hd v
else let s = vector_product(tl v) in
if s = <err>
then <err>
elseif is_Real(hd v)
then realmult(hd v,s)
else intmult(hd v,s);
vector_all: VectorValue -> Expressible_value
vector_all(v) ==
if len v = 1
then hd v
else let b = vector_all(tl v) in
if b = <err>
then <err>
else tr_and(hd v,b);
vector_some: VectorValue -> Expressible_value
vector_some(v) ==
if len v = 1
then hd v
else let b = vector_some(tl v) in
if b = <err>
then <err>
else tr_or(hd v,b);
vector_max: VectorValue -> Expressible_value
vector_max(v) ==
if len v = 1
then hd v
else let s = vector_max(tl v) in
if s = <err>
then <err>
elseif is_Real(hd v)
then realmax(hd v,s)
else intmax(hd v,s);
vector_min: VectorValue -> Expressible_value
vector_min(v) ==
if len v = 1
then hd v
else let s = vector_min(tl v) in
if s = <err>
then <err>
elseif is_Real(hd v)
then realmin(hd v,s)
else intmin(hd v,s);
vector_concat: Vector * Vector -> Vector
vector_concat(v1,v2) ==
let type = if tleq(v1.type.type,v2.type.type)
then v2.type.type
else v1.type.type,
lower = v1.type.lower,
upper = v1.type.upper + v2.type.upper - v2.type.lower + 1,
fl = v1.type.fl,
vec = v1.val^v2.val in
let new_type = mk_VectorType(lower,upper,type,fl) in
mk_Vector(vec,new_type);
widen_type: Expressible_value * Expressible_type -> Expressible_value
widen_type(x,type) ==
if x = <err> or is_Void(x)
then <err>
else mu(x,type |-> type);
const_type: Expressible_value -> (Expressible_type | Errvalue)
const_type(v) ==
if is_Void(v)
then v.type
elseif is_Vector(v)
then mk_VectorType(v.type.lower,v.type.upper,
seqlub([const_type(i) | i in seq v.val]),v.type.fl)
elseif is_Structure(v)
then mk_StructureType([const_type(construct_ev(v.val(i),v.type.tps(i)))
| i in set inds v.val],v.type.fl)
elseif is_Union(v)
then const_type(v.val)
elseif v = <err>
then <err>
elseif is_Real(v)
then mk_Float({mk_Floatrng(floor v.val, if
is_int(v.val) then v.val else floor(v.val + 0.5))},
v.type.abserr,v.type.relerr,v.type.fl)
elseif is_Int(v)
then mk_IntType(v.type.rep,{v.val},v.type.fl)
else mk_TrType({v.val},v.type.fl);
fleq: Expressible_type * Expressible_type -> bool
fleq(t1,t2) ==
if (is_VoidType(t1) and is_VoidType(t2)) then t1 = t2
elseif not (is_VoidType(t1) and is_VoidType(t2)) then t1.fl = t2.fl
else false;
replace_flavour: Expressible_type * Flavdom -> (Expressible_type|Errvalue)
replace_flavour(type,flav) ==
cases type:
mk_VoidType(fl) -> mk_VoidType(flav),
mk_TrType(r,f) -> mk_TrType(r,flav),
mk_Float(r,a,re,f) -> mk_Float(r,a,re,flav),
mk_IntType(rep,r,f) -> mk_IntType(rep,r,flav),
mk_VectorType(l,u,t,f) -> mk_VectorType(l,u,t,flav),
mk_UnionType(tps,fl) -> mk_UnionType(tps, flav),
mk_StructureType(tps,fl) -> mk_StructureType(tps, flav)
end;
lub: Expressible_type * Expressible_type -> (Expressible_type | Errvalue)
lub(t1,t2) ==
if is_TrType(t1) and is_TrType(t2) and fleq(t1,t2)
then trlub(t1,t2)
elseif is_Float(t1) and is_Float(t2) and fleq(t1,t2)
then floatlub(t1,t2)
elseif is_IntType(t1) and is_IntType(t2) and fleq(t1,t2)
then intlub(t1,t2)
elseif is_VectorType(t1) and is_VectorType(t2) and fleq(t1,t2)
then vectorlub(t1,t2)
elseif is_StructureType(t1) and is_StructureType(t2) and fleq(t1,t2)
then struclub(t1,t2)
elseif is_UnionType(t1) and is_UnionType(t2) and fleq(t1,t2)
then unionlub(t1,t2)
elseif is_VoidType(t1) and is_VoidType(t2) and fleq(t1,t2)
then t1
else <err>;
trlub : TrType * TrType -> TrType
trlub(t1,t2) ==
mk_TrType(t1.range union t2.range,t1.fl);
floatlub: Float * Float -> Float
floatlub(t1,t2) ==
mk_Float(t1.range union t2.range, max({t1.abserr,t2.abserr}),
max({t1.relerr,t2.relerr}),t1.fl);
intlub: IntType * IntType -> (IntType | Errvalue)
intlub(t1,t2) ==
if t1.rep = <byte> and t2.rep = <byte>
then mk_IntType(<byte>,t1.range union t2.range, t1.fl)
elseif t1.rep = <word> and t2.rep = <word>
then mk_IntType(<word>,t1.range union t2.range, t1.fl)
else <err>;
vectorlub : VectorType * VectorType -> (VectorType | Errvalue)
vectorlub(t1,t2) ==
if (t1.lower <> t2.lower) or (t1.upper <> t2.upper) or
(lub(t1.type,t2.type) = <err>)
then <err>
else mk_VectorType(t1.lower,t1.upper,lub(t1.type,t2.type),t1.fl);
struclub: StructureType * StructureType -> (StructureType | Errvalue)
struclub(t1,t2) ==
if len t1.tps <> len t2.tps
then <err>
elseif exists i in set inds t1.tps & lub(t1.tps(i),t2.tps(i)) = <err>
then <err>
else mk_StructureType([lub(t1.tps(i),t2.tps(i)) | i in set inds t1.tps],
t1.fl);
unionlub: UnionType * UnionType -> (UnionType | Errvalue)
unionlub(t1,t2) ==
if card t1.tps <> card t2.tps
then <err>
else let lub = setlub(t1.tps union t2.tps) in
if lub = <err>
then <err>
elseif is_UnionType(lub)
then mk_UnionType(lub.tps,t1.fl)
else mk_UnionType({lub},t1.fl);
seqlub: seq1 of Expressible_type -> (Expressible_type | Errvalue)
seqlub(tps) ==
if len tps = 1
then hd tps
elseif lub(tps(1),tps(2)) = <err>
then <err>
else lub(lub(tps(1),tps(2)),seqlub(tl tps));
setlub : set of Expressible_type -> (Expressible_type | Errvalue)
setlub(s) ==
if exists t1,t2 in set s & lub(t1,t2) = <err>
then if forall t in set s & is_TrType(t) or is_IntType(t) or
is_Float(t) or is_VoidType(t)
then let t1 = { setlub({ t' | t' in set s & is_TrType(t') and
t.fl = t'.fl}) | t in set s & is_TrType(t)},
t2 = { setlub({ t' | t' in set s & is_IntType(t') and
t.fl = t'.fl}) | t in set s & is_IntType(t)},
t3 = { setlub({ t' | t' in set s & is_Float(t') and
t.fl = t'.fl}) | t in set s & is_Float(t)},
t4 = { setlub({ t' | t' in set s & is_VoidType(t') and
t.fl = t'.fl}) | t in set s & is_VoidType(t)} in
if (exists t,t' in set dunion {t1,t2,t3,t4} & t.fl = t'.fl)
or exists t in set dunion {t1,t2,t3},
mk_VoidType(f) in set t4 &
t.fl = f
then <err>
else mk_UnionType(t1 union t2 union t3 union t4,{})
else <err>
else let t in set s in
if s = {t}
then t
else lub(t,setlub(s \ {t}));
gt : Expressible_type * Expressible_type -> bool
gt(t1,t2) ==
lub(t1,t2) = t1 or
(fleq(t1,t2) and
( (is_TrType(t2) and let z in set power {0,1} be st
true in set t2.range => 1 in set z and
false in set t2.range => 0 in set z in
(is_Float(t1) and z subset dunion {{lower,...,upper} |
mk_Floatrng(lower,upper) in set t1.range}) or
(is_IntType(t1) and z subset t1.range))
or
(is_IntType(t2) and t2.rep = <byte> and
(is_Float(t1) and t2.range subset
dunion {{lower,...,upper} | mk_Floatrng(lower,upper)
in set t1.range}) or
(is_IntType(t1) and t1.rep = <word> and t2.range subset t1.range))
or
(is_IntType(t2) and t2.rep = <word> and is_Float(t1) and
t2.range subset dunion {{lower,...,upper} |
mk_Floatrng(lower,upper) in set t1.range})
or
(is_Float(t2) and is_Float(t1) and
dunion { {lower,...,upper} | mk_Floatrng(lower,upper) in set
t2.range} subset
dunion { {lower,...,upper} | mk_Floatrng(lower,upper) in set
t1.range} and
t2.abserr + t2.relerr * max({ abs max({lower,upper}) |
mk_Floatrng(lower,upper) in set t2.range}) <= t1.abserr +
t1.relerr * max({ abs max({lower,upper}) |
mk_Floatrng(lower,upper) in set t1.range}))
or
(is_UnionType(t1) and is_UnionType(t2) and
forall t in set t1.tps & exists t' in set t2.tps &
lub(t,t') = t))
or
(is_UnionType(t2) and exists t in set t2.tps & gt(t1,t)));
tleq: Expressible_type * Expressible_type -> bool
tleq(t1,t2) ==
lub(t1,t2) = t2;
next_locn: Location -> Location
next_locn(mk_Location(l)) ==
mk_Location(l+1);
access: Location -> Store -> Storable_value
access(l)(s) ==
s(l);
update : Location -> Storable_value -> Store -> Store
update(l)(v)(s) ==
s ++ {l |-> v};
multi_update: seq of Location -> seq of Storable_value -> Store -> Store
multi_update(ls)(vs)(s) ==
if ls = []
then s
else multi_update(tl ls)(tl vs)(s ++ { hd ls |-> hd vs})
pre len ls = len vs;
timeleq : Time * Time -> bool
timeleq(mk_(lt1,ut1),mk_(lt2,ut2)) ==
lt2 <= lt1 and lt1 <= ut1 and ut1 <= ut2;
access_env : Id -> Env -> Denotable_value
access_env(i)(mk_(m,l)) ==
m(i);
update_env : Id -> Denotable_value -> Env -> Env
update_env(i)(d)(mk_(m,l)) ==
mk_(m ++ { i |-> d },l);
empty_env: Location -> Env
empty_env(l) ==
mk_({|->},l);
multi_update_env : seq of (Id * Denotable_value) -> Env -> Env
multi_update_env(s)(e) ==
if s = []
then e
else let mk_(id,v) = hd s in
multi_update_env (tl s)(update_env(id)(v)(e));
reserve_locn : Env -> (Location * Env)
reserve_locn(mk_(m,l)) ==
mk_(l,mk_(m,next_locn(l)));
instantiate_formals : (seq of Formal_elt) -> Param -> Env ->
(Env | Errvalue)
instantiate_formals(formals)(params)(e) ==
if len formals <> len params
then <err>
else let lubs_eq = [ lub(formals(i).rep, (params(i)).type) =
formals(i).rep | i in set inds formals] in
if false in set elems lubs_eq
then <err>
else let vals = [ if formals(i).fl = {}
then params(i)
else widen_type(params(i).val,
replace_flavour(params(i).type,
formals(i).fl)) | i in set inds params] in
multi_update_env([mk_(formals(i).id,vals(i)) | i in set
inds vals])(e);
mantissa : Real -> Real
mantissa(r) == r;
exponent : Real -> Real
exponent(r) == r;
tplus : Time * Time -> Time
tplus(mk_(l1,u1),mk_(l2,u2)) ==
mk_(l1 + l2, u1 + u2);
dtplus : seq of Time -> Time
dtplus(ts) ==
if ts = []
then zerot
else tplus(hd ts, dtplus(tl ts));
t_trimming_op:int -> Time
t_trimming_op(l) == mk_(1,1);
t_vector_extract: int -> Time
t_vector_extract(l) == mk_(1,1);
t_vector_concat: int * int -> Time
t_vector_concat(l,m) == mk_(1,1);
t_vectorsum: int -> Time
t_vectorsum(l) == mk_(1,1);
t_vectorproduct: int -> Time
t_vectorproduct(l) == mk_(1,1);
t_vector_all: int -> Time
t_vector_all(l) == mk_(1,1);
t_vector_some: int -> Time
t_vector_some(l) == mk_(1,1);
t_vector_max: int -> Time
t_vector_max(l) == mk_(1,1);
t_vector_min: int -> Time
t_vector_min(l) == mk_(1,1);
t_vector_flatten: int -> Time
t_vector_flatten(l) == mk_(1,1);
t_vector_subv: int -> Time
t_vector_subv(l) == mk_(1,1);
t_multi_update : int -> Time
t_multi_update(l) == mk_(1,1);
choose : Expressible_type -> Expressible_value
choose(tp) ==
let val: Expressible_value be st
lub(const_type(val),tp) = tp in
widen_type(const_type(val),tp);
eval_Program : Program -> Location -> Store -> EST_value
eval_Program(mk_Program(expr))(l)(sto) ==
eval_Expression(expr)(empty_env(l))(mk_PState(sto,zerot)) ;
eval_Expression : Expression -> Env -> PState -> EST_value
eval_Expression(mk_Expression(expr))(env)(ps) ==
cases expr:
mk_Operation(op) -> eval_Operation(expr)(env)(ps),
mk_InnerLoop(l) -> eval_InnerLoop(expr)(env)(ps),
mk_Assignment(a) -> eval_Assignment(expr)(env)(ps),
mk_Scope(s) -> eval_Scope(expr)(env)(ps),
mk_GuardedScope(d,i,o) -> eval_GuardedScope(expr)(env)(ps),
mk_Assertion(exp,tp) -> eval_Assertion(expr)(env)(ps),
mk_TimedExpression(t) -> eval_TimedExpression(expr)(env)(ps)
end;
eval_Operation : Operation -> Env -> PState -> EST_value
eval_Operation(mk_Operation(op))(e)(ps) ==
cases op:
mk_MonOperation(mo) -> eval_MonOperation(op)(e)(ps),
mk_BinaryOperation(l,bo,r) -> eval_BinaryOperation(op)(e)(ps)
end;
eval_MonOperation : MonOperation -> Env -> PState -> EST_value
eval_MonOperation(mk_MonOperation(mo))(e)(ps) ==
cases mo:
mk_MonOpMonOperand(opr,opnd) ->
eval_MonOpMonOperand(mk_MonOpMonOperand(opr,opnd))(e)(ps),
mk_VectorOperation(v,m,op) ->
eval_VectorOperation(mk_VectorOperation(v,m,op))(e)(ps),
mk_Value(v) -> eval_Value(mk_Value(v))(e)(ps)
end;
eval_MonOpMonOperand: MonOpMonOperand -> Env -> PState -> EST_value
eval_MonOpMonOperand(mk_MonOpMonOperand(opr,opnd))(e)(ps) ==
let x = eval_MonOperation(opnd)(e)(ps) in
if x.val = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else cases opr:
<numabs> -> eval_Abs(x),
<unaryminus> -> eval_MonMinus(x),
<not> -> eval_Not(x),
mk_CompileTimeOp(o) -> eval_CompileTimeOp(opr)(x),
<discard> -> eval_Discard(x),
<round> -> eval_Round(x),
<odd> -> eval_Odd(x),
<float> -> eval_Float(x),
<mantissa> -> eval_Mantissa(x),
<exponent> -> eval_Exponent(x)
end;
eval_Abs : EST_value -> EST_value
eval_Abs(mk_EST_value(val,sto,time)) ==
if is_Real(val)
then mk_EST_value(absreal(val),sto,tplus(time,t_absreal))
elseif is_Int(val)
then mk_EST_value(absint(val),sto,tplus(time,t_absint))
else mk_EST_value(<err>,sto,zerot);
eval_MonMinus : EST_value -> EST_value
eval_MonMinus(mk_EST_value(val,sto,time)) ==
if is_Real(val)
then mk_EST_value(realmonminus(val),sto,tplus(time,t_realmonminus))
elseif is_Int(val)
then mk_EST_value(intmonminus(val),sto,tplus(time,t_intmonminus))
else mk_EST_value(<err>,sto,zerot);
eval_Not : EST_value -> EST_value
eval_Not(mk_EST_value(val,sto,time)) ==
if not is_Tr(val)
then mk_EST_value(<err>, sto, zerot)
else mk_EST_value(tr_not(val),sto, tplus(time,t_not));
eval_CompileTimeOp : CompileTimeOp -> EST_value -> EST_value
eval_CompileTimeOp(mk_CompileTimeOp(op))(mk_EST_value(val,sto,time)) ==
if not is_Real(val)
then mk_EST_value(<err>,sto,zerot)
else cases op:
<inf> -> mk_EST_value(inf(val),sto,time),
<sup> -> mk_EST_value(sup(val),sto,time),
<absonly> -> mk_EST_value(absonly(val),sto,time),
<relonly> -> mk_EST_value(relonly(val),sto,time),
<abserr> -> mk_EST_value(abserr(val),sto,time),
<relerr> -> mk_EST_value(relerr(val),sto,time)
end;
eval_Discard : EST_value -> EST_value
eval_Discard(mk_EST_value(val,sto,time)) ==
if not is_Real(val)
then mk_EST_value(<err>,sto, zerot)
else mk_EST_value(discard(val),sto,tplus(time,t_discard));
eval_Round : EST_value -> EST_value
eval_Round(mk_EST_value(val,sto,time)) ==
if not is_Real(val)
then mk_EST_value(<err>,sto, zerot)
else mk_EST_value(round(val),sto,tplus(time,t_round));
eval_Mantissa : EST_value -> EST_value
eval_Mantissa(mk_EST_value(val,sto,time)) ==
if not is_Real(val)
then mk_EST_value(<err>,sto, zerot)
else mk_EST_value(mantissa(val),sto,tplus(time,t_mantissa));
eval_Exponent : EST_value -> EST_value
eval_Exponent(mk_EST_value(val,sto,time)) ==
if not is_Real(val)
then mk_EST_value(<err>,sto, zerot)
else mk_EST_value(exponent(val),sto,tplus(time,t_exponent));
eval_Odd : EST_value -> EST_value
eval_Odd(mk_EST_value(val,sto,time)) ==
if not is_Real(val)
then mk_EST_value(<err>,sto, zerot)
else mk_EST_value(odd(val),sto,tplus(time,t_odd));
eval_Float : EST_value -> EST_value
eval_Float(mk_EST_value(val,sto,time)) ==
if not is_Real(val)
then mk_EST_value(<err>,sto, zerot)
else mk_EST_value(float(val),sto,tplus(time,t_float));
eval_VectorOperation : VectorOperation -> Env -> PState -> EST_value
eval_VectorOperation(mk_VectorOperation(vo,mo,mult))(e)(ps) ==
let x = eval_MonOperation(mo)(e)(ps) in
if not is_Vector(x.val)
then mk_EST_value(<err>,ps.sto,zerot)
else let v = if mult = nil then x
else eval_VectorMult(mu(x,sto |-> ps.sto))(mult)(e) in
if v.val = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else cases vo:
<sum> -> eval_VectorSum(v),
<product> -> eval_VectorProduct(v),
<vecmax> -> eval_VectorMax(v),
<vecmin> -> eval_VectorMin(v),
<all> -> eval_VectorAll(v),
<some> -> eval_VectorSome(v),
<flatten> -> eval_VectorFlatten(v)
end;
eval_VectorMult : EST_value -> Multiple -> Env -> EST_value
eval_VectorMult(mk_EST_value(est_val,sto,time))(mk_Multiple(op,to_p))(e)
==
let mk_Vector(val,type) = est_val in
let b1 = eval_Operation(op)(e)(mk_PState(sto,time)) in
let b2 = eval_Operation(to_p)(e)(mk_PState(sto,b1.time)) in
if not (is_Int(b1.val) and is_Int(b2.val))
then mk_EST_value(<err>,sto,zerot)
elseif card(b1.val.type.range) <> 1 or card(b2.val.type.range) <> 1
then mk_EST_value(<err>,sto,zerot)
else let lower = min({b1.val.val,b2.val.val}),
upper = max({b1.val.val,b2.val.val}) in
if (lower < type.lower) or (type.upper < upper)
then mk_EST_value(<err>,sto,zerot)
else let new_val = vector_subv(val,lower,upper),
new_type = mk_VectorType(lower,upper,type.type,type.fl) in
let new_v = mk_Vector(new_val,new_type),
new_t = tplus(tplus(b2.time,t_vector_subv(upper - lower)),
tplus(t_min,t_max)) in
mk_EST_value(new_v,sto,new_t);
eval_VectorSum : EST_value -> EST_value
eval_VectorSum(mk_EST_value(mk_Vector(val,type),sto,time)) ==
if is_Float(type.type) or is_IntType(type.type)
then mk_EST_value(vector_sum(val),sto,
tplus(time,t_vectorsum(type.upper - type.lower)))
else mk_EST_value(<err>,sto,zerot);
eval_VectorProduct : EST_value -> EST_value
eval_VectorProduct(mk_EST_value(mk_Vector(val,type),sto,time)) ==
if is_Float(type.type) or is_IntType(type.type)
then mk_EST_value(vector_product(val),sto,
tplus(time,t_vectorproduct(type.upper - type.lower)))
else mk_EST_value(<err>,sto,zerot);
eval_VectorMax : EST_value -> EST_value
eval_VectorMax(mk_EST_value(mk_Vector(val,type),sto,time)) ==
if is_Float(type.type) or is_IntType(type.type)
then mk_EST_value(vector_max(val),sto,
tplus(time,t_vector_max(type.upper - type.lower)))
else mk_EST_value(<err>,sto,zerot);
eval_VectorMin : EST_value -> EST_value
eval_VectorMin(mk_EST_value(mk_Vector(val,type),sto,time)) ==
if is_Float(type.type) or is_IntType(type.type)
then mk_EST_value(vector_min(val),sto,
tplus(time,t_vector_min(type.upper - type.lower)))
else mk_EST_value(<err>,sto,zerot);
eval_VectorAll : EST_value -> EST_value
eval_VectorAll(mk_EST_value(mk_Vector(val,type),sto,time)) ==
if not is_TrType(type.type)
then mk_EST_value(<err>,sto,zerot)
else mk_EST_value(vector_all(val),sto,
tplus(time,t_vector_all(type.upper - type.lower)));
eval_VectorSome : EST_value -> EST_value
eval_VectorSome(mk_EST_value(mk_Vector(val,type),sto,time)) ==
if not is_TrType(type.type)
then mk_EST_value(<err>,sto,zerot)
else mk_EST_value(vector_some(val),sto,
tplus(time,t_vector_some(type.upper - type.lower)));
eval_VectorFlatten : EST_value -> EST_value
eval_VectorFlatten(mk_EST_value(mk_Vector(val,type),sto,time)) ==
if not is_VectorType(type.type)
then mk_EST_value(<err>,sto,zerot)
else let new_val = vector_flatten(val) in
let new_upper = len new_val + type.lower - 1 in
let new_time = tplus(time,t_vector_flatten(type.upper -
type.lower)),
new_type = mk_VectorType(type.lower,
new_upper,type.type,type.fl) in
mk_EST_value(mk_Vector(new_val,new_type),sto,new_time);
eval_BinaryOperation: BinaryOperation -> Env -> PState -> EST_value
eval_BinaryOperation(bo)(e)(ps) ==
let mk_BinaryOp(op) = bo.opr in
cases op:
mk_NumOp(opr) -> eval_NumOp(bo)(e)(ps),
<numgt>,<numlt>,<numge>,<numle> -> eval_CompOp(bo)(e)(ps),
<and>,<or> -> eval_BoolOp(bo)(e)(ps),
<EQ>,<NEQ> -> eval_EqOp(bo)(e)(ps),
<concat> -> eval_Concat(bo)(e)(ps)
end;
eval_NumOp : BinaryOperation -> Env -> PState -> EST_value
eval_NumOp(mk_BinaryOperation(left,mk_BinaryOp(opr),right))(e)(ps) ==
let a1 = eval_MonOperation(left)(e)(ps) in
let a2 = eval_MonOperation(right)(e)(mu(ps, time |-> a1.time)) in
cases opr:
mk_NumOp(op) ->
cases mk_(a1.val,a2.val):
mk_(mk_Int(v1,t1),mk_Int(v2,t2)) ->
if op <> <numdiv>
then let val = intbinop(mk_Int(v1,t1),mk_Int(v2,t2),mk_NumOp(op)) in
if val = <err>
then mk_EST_value(<err>, ps.sto, zerot)
else mk_EST_value(val,ps.sto, tplus(a2.time,t_intbinop))
else mk_EST_value(<err>,ps.sto,zerot),
mk_(mk_Real(v1,t1),mk_Real(v2,t2)) ->
if op not in set {<numdiv>,<nummod>}
then let val = realbinop(mk_Real(v1,t1),mk_Real(v2,t2),mk_NumOp(op))
in
if val = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else mk_EST_value(val,ps.sto, tplus(a2.time,t_realbinop))
else mk_EST_value(<err>,ps.sto,zerot),
others -> mk_EST_value(<err>,ps.sto,zerot)
end,
<replaceflav> -> if a2.val <> <err> and is_Void(a2.val)
then let mk_VoidType(f) = a2.val.type in
mk_EST_value(mu(a1.val,type |->
replace_flavour(a1.val.type,f)),
ps.sto,a2.time)
else mk_EST_value(<err>,ps.sto, zerot),
others -> mk_EST_value(<err>,ps.sto,zerot)
end;
eval_CompOp : BinaryOperation -> Env -> PState -> EST_value
eval_CompOp(mk_BinaryOperation(left,mk_BinaryOp(opr),right))(e)(ps) ==
let a1 = eval_MonOperation(left)(e)(ps) in
let a2 = eval_MonOperation(right)(e)(mu(ps, time |-> a1.time)) in
if (is_Int(a1.val) and is_Int(a2.val))
then mk_EST_value(intcomp(a1.val,a2.val,opr),
ps.sto,tplus(a2.time,t_intcomp))
elseif is_Real(a1.val) and is_Real(a2.val)
then mk_EST_value(realcomp(a1.val,a2.val,opr),
ps.sto,tplus(a2.time,t_realcomp))
else mk_EST_value(<err>, ps.sto, zerot);
eval_EqOp : BinaryOperation -> Env -> PState -> EST_value
eval_EqOp(mk_BinaryOperation(left,mk_BinaryOp(op),right))(e)(ps)==
let a1 = eval_MonOperation(left)(e)(ps) in
let a2 = eval_MonOperation(right)(e)(mu(ps, time |-> a1.time)) in
if is_Tr(a1.val) and is_Tr(a2.val)
then mk_EST_value(tr_eq(a1.val,a2.val,op),
ps.sto,tplus(a2.time,t_tr_eq))
elseif is_Real(a1.val) and is_Real(a2.val)
then mk_EST_value(real_eq(a1.val,a2.val,op),
ps.sto,tplus(a2.time,t_real_eq))
elseif is_Int(a1.val) and is_Int(a2.val)
then mk_EST_value(int_eq(a1.val,a2.val,op),
ps.sto,tplus(a2.time,t_int_eq))
elseif is_Void(a1.val) and is_Void(a2.val)
then mk_EST_value(void_eq(a1.val,a2.val,op),
ps.sto,tplus(a2.time,t_void_eq))
else mk_EST_value(<err>,ps.sto,zerot);
eval_BoolOp : BinaryOperation -> Env -> PState -> EST_value
eval_BoolOp(mk_BinaryOperation(left,mk_BinaryOp(op),right))(e)(ps) ==
let a1 = eval_MonOperation(left)(e)(ps) in
let a2 = eval_MonOperation(right)(e)(mu(ps, time |-> a1.time)) in
if not (is_Tr(a2.val) and is_Tr(a2.val))
then mk_EST_value(<err>,ps.sto,zerot)
else cases op:
<and> -> mk_EST_value(tr_and(a1.val,a2.val),ps.sto,
tplus(a2.time,t_and)),
<or> -> mk_EST_value(tr_or(a1.val,a2.val),ps.sto,
tplus(a2.time,t_and))
end;
eval_Concat : BinaryOperation -> Env -> PState -> EST_value
eval_Concat(mk_BinaryOperation(left,op,right))(e)(ps)==
let a1 = eval_MonOperation(left)(e)(ps) in
let a2 = eval_MonOperation(right)(e)(mu(ps, time |-> a1.time)) in
if not (is_Vector(a1.val) and is_Vector(a2.val))
then mk_EST_value(<err>,ps.sto,zerot)
elseif not (tleq(a1.val.type.type,a2.val.type.type) or
tleq(a2.val.type.type,a1.val.type.type))
then mk_EST_value(<err>, ps.sto,zerot)
else let new_vec = vector_concat(a1.val,a2.val),
new_time = tplus(a2.time,
t_vector_concat(vector_length(a1.val.type),
vector_length(a2.val.type))) in
mk_EST_value(new_vec,ps.sto,new_time);
eval_Value: Value -> Env -> PState -> EST_value
eval_Value(mk_Value(val))(e)(ps) ==
cases val:
mk_ConstantValue(c) -> eval_ConstantValue(mk_ConstantValue(c))(ps),
mk_NamedValue(n) -> eval_NamedValue(mk_NamedValue(n))(e)(ps),
mk_VectorVal(v) -> eval_VectorVal(mk_VectorVal(v))(e)(ps),
mk_StructureValue(s) -> eval_StructureValue(mk_StructureValue(s))(e)(ps),
mk_Sequence(s) -> eval_Sequence(mk_Sequence(s))(e)(ps),
mk_Call(id,acts) -> eval_Call(mk_Call(id,acts))(e)(ps),
mk_Conditional(c) -> eval_Conditional(val)(e)(ps),
mk_Widening(exp,t) -> eval_Widening(val)(e)(ps),
mk_OuterLoop(l) -> eval_OuterLoop(val)(e)(ps)
end;
eval_ConstantValue : ConstantValue -> PState -> EST_value
eval_ConstantValue(mk_ConstantValue(cv))(ps) ==
cases cv:
mk_IntegerDenotation(z) ->
let rep = if abs z >= bytemax then <word> else <byte> in
mk_EST_value(mk_Int(z,mk_IntType(rep,{z},{})),ps.sto,ps.time),
mk_FloatingDenotation(r) ->
mk_EST_value(mk_Real(r,mk_Float({mk_Floatrng(floor r, if
is_int(r) then r else floor (r +
0.5))},0,0,{})),ps.sto,ps.time),
mk_BooleanDenotation(b) ->
mk_EST_value(mk_Tr(b,mk_TrType({b},{})),ps.sto,ps.time),
mk_Ascii_Char(c) ->
mk_EST_value(mk_Int(ascii(c),mk_IntType(<byte>,{ascii(c)},{})),
ps.sto, ps.time),
mk_Ascii_string(s) ->
mk_EST_value(mk_Vector([mk_Int(ascii(a),
mk_IntType(<byte>,{ascii(a)}, {}))
| a in seq s],
mk_VectorType(1,len s, seqlub([mk_IntType(<byte>,
{ascii(a)},{}) | a in seq s]),{})),ps.sto,ps.time),
mk_Flavouring(fl) ->
mk_EST_value(mk_Void(<nil>, mk_VoidType(eval_Flavouring(cv))), ps.sto, ps.time),
<skip> -> mk_EST_value(mk_Void(<nil>,mk_VoidType({})), ps.sto,
tplus(ps.time, t_skip))
end;
eval_NamedValue : NamedValue -> Env -> PState -> EST_value
eval_NamedValue(mk_NamedValue(nv))(e)(ps) ==
cases nv :
mk_FlavourExtract(n,fl) -> eval_FlavourExtract(nv)(e)(ps),
mk_FlavourStrip(n,fl) -> eval_FlavourStrip(nv)(e)(ps),
mk_VectorExtract(n,i) -> eval_VectorExtract(nv)(e)(ps),
mk_VectorTrimming(n,t,i) -> eval_VectorTrimming(nv)(e)(ps),
others -> eval_Identifier(nv)(e)(ps)
end;
eval_Identifier : Id -> Env -> PState -> EST_value
eval_Identifier(id)(mk_(m,l))(mk_PState(sto,time)) ==
if id in set dom m
then cases access_env(id)(mk_(m,l)):
mk_Location(l) -> let mk_Storable_value(v) =
access (mk_Location(l))(sto) in
mk_EST_value(v,sto,tplus(time,t_access)),
mk_Storable_value(v) -> mk_EST_value(v,sto,time)
end
else mk_EST_value(<err>,sto,time);
eval_FlavourExtract : FlavourExtract -> Env -> PState -> EST_value
eval_FlavourExtract(mk_FlavourExtract(nv,fl))(e)(ps) ==
let n = eval_NamedValue(nv)(e)(ps),
f = eval_Flavouring(fl) in
if not is_Structure(n.val)
then mk_EST_value(<err>,ps.sto,ps.time)
else mk_EST_value(comp_extract(n.val,f),ps.sto,tplus(n.time,t_comp_extract));
eval_Flavouring : Flavouring -> Flavdom
eval_Flavouring(mk_Flavouring(fls)) ==
if fls = []
then {}
else {eval_Flavour(hd fls)} union eval_Flavouring(mk_Flavouring(tl fls));
eval_Flavour : Flavour -> Fl_elt
eval_Flavour(mk_Flavour(name,index)) ==
mk_Fl_elt(name,index);
eval_FlavourStrip : FlavourStrip -> Env -> PState -> EST_value
eval_FlavourStrip(mk_FlavourStrip(nv,fl))(e)(ps) ==
let n = eval_NamedValue(nv)(e)(ps),
f = eval_Flavouring(fl) in
if not is_Structure(n.val)
then mk_EST_value(<err>,ps.sto,ps.time)
else let n' = comp_extract(n.val,f) in
let n'' = mk_Structure(n'.val,mk_StructureType(n'.type.tps,{})) in
mk_EST_value(n'',ps.sto,tplus(n.time,t_comp_extract));
eval_VectorExtract : VectorExtract -> Env -> PState -> EST_value
eval_VectorExtract(mk_VectorExtract(n,i))(e)(ps) ==
let x = eval_NamedValue(n)(e)(ps) in
if not is_Vector(x.val)
then mk_EST_value(<err>,ps.sto,ps.time)
else let index = eval_Operation(i)(e)(mu(ps, time |-> x.time)),
length = x.val.type.upper - x.val.type.lower + 1 in
if not is_Int(index.val)
then mk_EST_value(<err>,ps.sto,ps.time)
elseif not (index.val.type.range subset
{x.val.type.lower,...,x.val.type.upper})
then mk_EST_value(<err>,ps.sto,ps.time)
else mk_EST_value(vector_extract(x.val,index.val.val),
ps.sto,tplus(index.time,t_vector_extract(length)));
eval_VectorTrimming : VectorTrimming -> Env -> PState -> EST_value
eval_VectorTrimming(mk_VectorTrimming(name,to_p,ctv))(e)(ps)==
let vec = eval_NamedValue(name)(e)(ps) in
if not is_Vector(vec.val) or (is_Vector(vec.val) and
not (is_Float(vec.val.type.type) or is_IntType(vec.val.type.type)))
then mk_EST_value(<err>,ps.sto,zerot)
else let v = eval_CompileTimeValue(ctv)(e) in
if not (is_Real(v.val) or is_Int(v.val))
then mk_EST_value(<err>,ps.sto,zerot)
else let new_v = cases to_p:
<gtvalue> ->
[i | i in seq vec.val.val & i >= v.val.val],
<ltvalue> ->
[i | i in seq vec.val.val & i <= v.val.val],
<atvalue> ->
[i | i in seq vec.val.val & i = v.val.val]
end in
if new_v = []
then mk_EST_value(<err>,ps.sto,zerot)
else let new_l = vec.val.type.lower,
new_u = vec.val.type.lower + len new_v - 1,
new_t = seqlub([const_type(v) | v in seq new_v]),
new_fl = vec.val.type.fl in
let new_vec = mk_Vector(new_v,mk_VectorType(new_l,new_u,new_t,
new_fl)),
new_time = tplus(vec.time,
t_trimming_op(new_u-new_l)) in
mk_EST_value(new_vec,ps.sto,new_time);
eval_CompileTimeValue : CompileTimeValue -> Env -> EST_value
eval_CompileTimeValue(mk_CompileTimeValue(op))(mk_(m,l)) ==
let locs = {id | id in set dom m & is_Location(m(id))} in
let new_m = locs <-: m in
let new_env = mk_(new_m,l) in
eval_Operation(op)(new_env)(mk_PState({|->},zerot));
eval_VectorVal : VectorVal -> Env -> PState -> EST_value
eval_VectorVal(mk_VectorVal(ops))(e)(ps) ==
let vals = [ eval_Operation(o)(e)(mk_PState(ps.sto,zerot)) | o in seq ops] in
let val = [ v.val | v in seq vals],
time = dtplus([v.time | v in seq vals]) in
if <err> in set elems val
then mk_EST_value(<err>,ps.sto,zerot)
else let type = seqlub([v.type | v in seq val]) in
if type = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else let tp = mk_VectorType(1,len val, type, {}) in
let x = mk_Vector(val,tp) in
mk_EST_value(x,ps.sto,time);
eval_StructureValue: StructureValue -> Env -> PState -> EST_value
eval_StructureValue(mk_StructureValue(ops))(e)(ps) ==
let vals = [ eval_Operation(o)(e)(mk_PState(ps.sto,zerot)) | o in seq ops] in
if (exists val in seq vals &
not (is_Tr(val.val) or is_Int(val.val) or is_Real(val.val)))
then mk_EST_value(<err>,ps.sto,zerot)
elseif exists v1,v2 in seq vals & fleq(v1.val.type,v2.val.type)
then mk_EST_value(<err>,ps.sto, zerot)
else let tps = [v.val.type | v in seq vals],
time = dtplus([v.time | v in seq vals]),
comps = [v.val.val | v in seq vals] in
let type = mk_StructureType(tps,{}) in
let val = mk_Structure(comps,type) in
mk_EST_value(val,ps.sto,time);
eval_Sequence : Sequence -> Env -> PState -> EST_value
eval_Sequence(mk_Sequence(exprs))(e)(ps) ==
let x = eval_Expression(hd exprs)(e)(ps) in
if len exprs = 1
then x
elseif is_Void(x.val)
then eval_Sequence(mk_Sequence(tl exprs))(e)(mk_PState(x.sto,x.time))
else mk_EST_value(<err>,ps.sto,zerot);
eval_Call : Call -> Env -> PState -> EST_value
eval_Call(mk_Call(id,acts))(mk_(m,l))(mk_PState(sto,time)) ==
if id not in set dom m
then mk_EST_value(<err>,sto,zerot)
else let pp = access_env(id)(mk_(m,l)) in
if not is_Proc(pp)
then mk_EST_value(<err>,sto,zerot)
else let mk_Proc(p) = pp in
let params = eval_Acts(acts)(mk_(m,l))(
mk_PState(sto,time)) in
if <err> in set {x.val | x in seq params}
then mk_EST_value(<err>,sto,zerot)
else p([m.val | m in seq params])
(mk_PState(sto, params(len params).time));
eval_Acts: seq of Operation -> Env -> PState -> seq of EST_value
eval_Acts(ops)(e)(ps) ==
if ops = []
then []
else let x = eval_Operation(hd ops)(e)(ps) in
[x]^eval_Acts(tl ops)(e)(mk_PState(ps.sto,x.time));
eval_Widening : Widening -> Env -> PState -> EST_value
eval_Widening(mk_Widening(expr,dest_type))(e)(ps) ==
let x = eval_Expression(expr)(e)(ps) in
if x.val = <err>
then mk_EST_value(<err>, ps.sto, zerot)
else let xt = x.val.type,
dt = eval_Type(dest_type)(e) in
if dt=<err>
then mk_EST_value(<err>, ps.sto, zerot)
else let dt' = phi_remove(dt) in
if gt(dt',xt)
then mk_EST_value(widen_type(x.val,dt'), ps.sto, x.time)
else mk_EST_value(<err>, ps.sto, zerot);
eval_Type : Type -> Env -> (Expressible_type | Errvalue)
eval_Type(mk_Type(tp))(e) ==
cases tp:
mk_PrimitiveType(p) -> eval_PrimitiveType(tp)(e),
mk_VecType(range,tpe) -> eval_VecType(tp)(e),
mk_StrucType(tps) -> eval_StrucType(tp)(e),
mk_FlavouredType(fl,tpe) -> eval_FlavouredType(tp)(e),
mk_UnionTp(tps) -> eval_UnionTp(tp)(e),
mk_TypeName(id) -> eval_TypeName(tp)(e)
end;
eval_PrimitiveType : PrimitiveType -> Env -> (Expressible_type | Errvalue)
eval_PrimitiveType(mk_PrimitiveType(pt))(e) ==
if is_Number(pt)
then eval_Number(pt)(e)
elseif is_FloatType(pt)
then eval_FloatType(pt)(e)
else eval_VoidValType(pt)(e);
eval_Number : Number -> Env -> (Expressible_type | Errvalue)
eval_Number(mk_Number(rep,range))(e) ==
let ranges = { eval_Range(r)(e) | r in seq range} in
if <err> in set ranges
then <err>
elseif rep = <bit>
then if exists v in set dunion ranges & v not in set {0,1}
then <err>
else let m = { 0 |-> false, 1 |-> true} in
mk_TrType({m(v) | v in set dunion ranges},{})
elseif rep = <byte>
then if exists v in set dunion ranges & abs v > bytemax
then <err>
else mk_IntType(rep,dunion ranges, {})
elseif exists v in set dunion ranges & abs v > maxint
then <err>
else mk_IntType(rep,dunion ranges, {});
eval_Range : Range -> Env -> (set of int | Errvalue)
eval_Range(mk_Range(lower,upper))(e) ==
if (lower = nil and upper = nil) or
(lower <> nil and not is_Int((eval_CompileTimeValue(lower)(e)).val)) or
(upper <> nil and not is_Int((eval_CompileTimeValue(upper)(e)).val))
then <err>
elseif lower=nil
then { x | x: int & 0 <= x and x <= (eval_CompileTimeValue(upper)(e)).val.val}
elseif upper = nil
then { x | x: int & (eval_CompileTimeValue(lower)(e)).val.val <= x and
x <= maxint}
else { x | x: int & (eval_CompileTimeValue(lower)(e)).val.val <= x and
x <= (eval_CompileTimeValue(upper)(e)).val.val};
eval_FloatType : FloatType -> Env -> (Expressible_type | Errvalue)
eval_FloatType(mk_FloatType(ranges,abserr,relerr))(e) ==
if (abserr = nil and relerr = nil) or
(exists range in seq ranges & (eval_Range(range)(e)) = <err>)
then <err>
else let abse = if abserr = nil
then mk_Real(0,mk_Float({mk_Floatrng(0,0)},0,0,{}))
else (eval_CompileTimeValue(abserr)(e)).val,
rele = if relerr = nil
then mk_Real(0,mk_Float({mk_Floatrng(0,0)},0,0,{}))
else (eval_CompileTimeValue(relerr)(e)).val in
if not(is_Real(abse) and is_Real(rele))
then <err>
else mk_Float({mk_Floatrng(min(eval_Range(range)(e)),
max(eval_Range(range)(e))) | range
in seq ranges}, abse.val,rele.val,{});
eval_VoidValType : VoidValType -> (Env -> (Expressible_type | Errvalue))
eval_VoidValType(fl) ==
lambda e: Env & mk_VoidType(eval_Flavouring(fl));
eval_StrucType : StrucType -> Env -> (Expressible_type | Errvalue)
eval_StrucType(mk_StrucType(tps))(e) ==
let typs = [ eval_Type(t)(e) | t in seq tps] in
if exists tp in seq typs &
not (is_TrType(tp) or is_Float(tp) or is_IntType(tp))
then <err>
elseif exists tp1,tp2 in seq typs &
tp1 <> tp2 and tp1.fl = tp2.fl
then <err>
else mk_StructureType(typs,{});
eval_VecType : VecType -> (Env -> (Expressible_type | Errvalue))
eval_VecType(mk_VecType(range,tp)) == lambda e : Env &
let typ = eval_Type(tp)(e),
nrange = eval_Range(range)(e) in
if typ = <err> or nrange = <err>
then <err>
else mk_VectorType(min(nrange),max(nrange),typ,{});
eval_FlavouredType : FlavouredType -> Env -> (Expressible_type | Errvalue)
eval_FlavouredType(mk_FlavouredType(fl,tp))(e) ==
let flavour = eval_Flavouring(fl),
typ = eval_Type(tp)(e) in
if typ = <err>
then <err>
else cases typ:
mk_VoidType(t) -> mk_VoidType(t union flavour),
mk_TrType(range,fl) -> mk_TrType(range,fl union flavour),
mk_IntType(rep,range,fl) -> mk_IntType(rep,range, fl union flavour),
mk_Float(range,abse,rele,fl) -> mk_Float(range,abse,rele,fl union flavour),
mk_VectorType(lower,upper,tp,fl) ->
mk_VectorType(lower,upper,tp, fl union flavour),
mk_StructureType(tps,fl) -> mk_StructureType(tps,fl union flavour),
mk_UnionType(tps,fl) -> mk_UnionType(tps,fl union flavour)
end;
eval_UnionTp : UnionTp -> Env -> (Expressible_type | Errvalue)
eval_UnionTp(mk_UnionTp(tps))(e) ==
let typs = {eval_Type(t)(e) | t in seq tps} in
if exists tp in set typs & not (is_IntType(tp) or is_Float(tp) or
is_TrType(tp) or is_VoidType(tp))
then <err>
elseif exists t1,t2 in set typs & fleq(t1,t2)
then <err>
else mk_UnionType(typs,{});
eval_TypeName : TypeName -> Env -> (Expressible_type | Errvalue)
eval_TypeName(mk_TypeName(id))(mk_(m,l)) ==
if id in set dom m
then cases access_env(id)(mk_(m,l)):
mk_Location(l),mk_Storable_value(v),
mk_Proc(p),<err> -> <err>,
t -> t
end
else <err>;
eval_Scope : Scope -> Env -> PState -> EST_value
eval_Scope(mk_Scope(s))(e)(ps) ==
if is_SimpleScope(s)
then eval_SimpleScope(s)(e)(ps)
else eval_PackageScope(s)(e)(ps);
eval_SimpleScope : SimpleScope -> Env -> PState -> EST_value
eval_SimpleScope(mk_SimpleScope(decls,expr))(e)(ps) ==
let old_env_st = mk_(e,ps) in
let new_env_st = eval_Decls(decls)(old_env_st) in
if new_env_st = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else let mk_(new_env,new_sto) = new_env_st in
eval_Expression(expr)(new_env)(new_sto);
eval_Decls: seq of Declaration -> EnvState -> EnvState
eval_Decls(decls)(env_st) ==
if env_st = <err>
then <err>
elseif decls = []
then env_st
else eval_Decls(tl decls)(eval_Declaration(hd decls)(env_st));
eval_Declaration : Declaration -> EnvState -> EnvState
eval_Declaration(decl)(env_st) ==
cases decl :
mk_ImportDecl(id,tp) -> eval_ImportDecl(decl)(env_st),
mk_ExportDecl(id,expr) -> eval_ExportDecl(decl)(env_st),
mk_LetDecl(l) -> eval_LetDecl(decl)(env_st),
mk_VarDecl(id,expr) -> eval_VarDecl(decl)(env_st),
mk_ProcDec(nls,ph,expr) -> eval_ProcDec(decl)(env_st),
mk_TypeDec(id,type) -> eval_TypeDec(decl)(env_st)
end;
eval_ImportDecl : ImportDecl -> EnvState -> EnvState
eval_ImportDecl(mk_ImportDecl(id,tp))(mk_(e,ps)) ==
let type = eval_Type(tp)(e) in
if type = <err>
then <err>
else let val = choose(type),
mk_(l,n_e) = reserve_locn(e) in
let nn_e = update_env(id)(l)(n_e),
sto = update(l)(mk_Storable_value(val))(ps.sto),
t = tplus(ps.time,t_update) in
mk_(nn_e,mk_PState(sto,t));
eval_ExportDecl : ExportDecl -> EnvState -> EnvState
eval_ExportDecl(mk_ExportDecl(id,expr))(mk_(e,ps)) ==
let x = eval_Expression(expr)(e)(ps) in
if x.val = <err>
then <err>
else let mk_(l,n_e) = reserve_locn(e) in
let nn_e = update_env(id)(l)(n_e),
sto = update(l)(mk_Storable_value(x.val))(ps.sto),
t = tplus(ps.time,t_update) in
mk_(nn_e,mk_PState(sto,t));
eval_LetDecl : LetDecl -> EnvState -> EnvState
eval_LetDecl(mk_LetDecl(decl))(es) ==
if is_SimpleLetDecl(decl)
then eval_SimpleLetDecl(decl)(es)
else eval_StrucLetDecl(decl)(es);
eval_SimpleLetDecl : SimpleLetDecl -> EnvState -> EnvState
eval_SimpleLetDecl(mk_SimpleLetDecl(id,expr))(mk_(e,ps)) ==
let x = eval_Expression(expr)(e)(ps) in
if x.val = <err>
then <err>
else mk_((update_env(id)(x.val)(e)),
mk_PState(ps.sto, x.time));
eval_StrucLetDecl : StrucLetDecl -> EnvState -> EnvState
eval_StrucLetDecl(mk_StrucLetDecl(ids,expr))(mk_(e,ps)) ==
let x = eval_Expression(expr)(e)(ps) in
if not is_Structure(x.val)
then <err>
elseif len ids <> struc_length(x.val.type)
then <err>
else let id_vals = [ mk_(ids(i),
construct_ev(x.val.val(i),x.val.type.tps(i))) |
i in set inds ids] in
let new_env = multi_update_env(id_vals)(e) in
mk_(new_env,mk_PState(ps.sto,x.time));
eval_VarDecl : VarDecl -> EnvState -> EnvState
eval_VarDecl(mk_VarDecl(id,expr))(mk_(e,ps)) ==
let x = eval_Expression(expr)(e)(ps) in
if x.val = <err>
then <err>
else let mk_(l,n_e) = reserve_locn(e) in
let nn_e = update_env(id)(l)(n_e),
sto = update(l)(mk_Storable_value(x.val))(ps.sto),
t = tplus(ps.time,t_update) in
mk_(nn_e,mk_PState(sto,t));
eval_ProcDec : ProcDec -> EnvState -> EnvState
eval_ProcDec(mk_ProcDec(nls,ph,expr))(mk_(e,ps)) ==
let env_st = eval_NonLocals(nls)(e)(ps) in
if env_st = <err>
then <err>
else let mk_ProcHeading(id,formals) = ph,
mk_(ne,ns) = env_st in
let fls = eval_Formals(formals)(e) in
let pr =
mk_Proc(lambda a:Param &
let nn_e = instantiate_formals(fls)(a)(ne) in
lambda nps: PState &
if nn_e = <err>
then mk_EST_value(<err>,nps.sto,zerot)
else let x = eval_Expression(expr)(nn_e)(nps) in
if x.val <> <err> and
((is_Void(x.val) and x.val.type = mk_VoidType({Phi}))
or
(not is_Void(x.val) and x.val.type.fl = {Phi}))
then mk_EST_value(<err>,nps.sto,zerot)
else x) in
mk_(update_env(id)(pr)(e),mk_PState(ps.sto, ns.time));
eval_NonLocals : NonLocals -> Env -> PState -> EnvState
eval_NonLocals(mk_NonLocals(ids,decls))(mk_(m,l))(ps) ==
let ids_map = if ids = nil then {|->} else (elems ids) <: m in
if decls = nil
then mk_(mk_(ids_map,l),ps)
else eval_Decls(decls)(mk_(mk_(ids_map,l),ps));
eval_Formals : seq of Formal -> Env -> seq of Formal_elt
eval_Formals(fls)(e) ==
[eval_Formal(f)(e) | f in seq fls];
eval_Formal : Formal -> Env -> Formal_elt
eval_Formal(mk_Formal(id,rep,fl))(e) ==
let n_rep = eval_Representation(rep)(e),
n_fl = eval_Flavouring(fl) in
mk_Formal_elt(id,n_rep,n_fl);
eval_Representation : Representation -> Env -> (Expressible_type | Errvalue)
eval_Representation(rep)(e) ==
cases rep:
mk_PrimitiveRep(p) -> eval_PrimitiveRep(rep)(e),
mk_StrucRep(rs) -> eval_StrucRep(rep)(e),
mk_VecRep(range,r) -> eval_VecRep(rep)(e),
mk_UnionRep(rs) -> eval_UnionRep(rep)(e),
mk_FlavouredRep(f,r) -> eval_FlavouredRep(rep)(e),
mk_Type(t) -> eval_Type(rep)(e)
end;
eval_PrimitiveRep : PrimitiveRep -> Env -> (Expressible_type | Errvalue)
eval_PrimitiveRep(mk_PrimitiveRep(rep))(e) ==
if is_NumRep(rep)
then eval_NumRep(rep)(e)
else eval_FloatRep(rep)(e);
eval_NumRep : NumRep -> Env -> (Expressible_type | Errvalue)
eval_NumRep(mk_NumRep(rep,range))(e) ==
let ranges = if range = nil then {}
else {eval_Range(r)(e) | r in seq range} in
if <err> in set ranges
then <err>
elseif rep = <bit>
then if exists v in set dunion ranges & v not in set {0,1}
then <err>
else let rngs = if range = nil then {true,false}
else {{0 |-> false, 1 |-> true}(r) | r in set
dunion ranges} in
mk_TrType(rngs,{})
elseif rep = <byte>
then if exists v in set dunion ranges & abs v > bytemax
then <err>
else let rngs = if range = nil then {-bytemax,...,bytemax}
else dunion ranges in
mk_IntType(rep,rngs,{})
elseif exists v in set dunion ranges & abs v > maxint
then <err>
else let rngs = if range = nil then {-maxint,...,maxint}
else dunion ranges in
mk_IntType(rep,rngs,{});
eval_FloatRep : FloatRep -> Env -> (Expressible_type | Errvalue)
eval_FloatRep(mk_FloatRep(range,abserr,relerr))(e) ==
let ranges = if range = nil then {}
else {eval_Range(r)(e) | r in seq range},
abse = if abserr = nil
then mk_Real(maxint,
mk_Float({mk_Floatrng(maxint,maxint)},0,0,{}))
else eval_CompileTimeValue(abserr)(e),
rele = if relerr = nil
then mk_Real(maxint,
mk_Float({mk_Floatrng(maxint,maxint)},0,0,{}))
else eval_CompileTimeValue(relerr)(e) in
if not (is_Real(abse.val) and is_Real(rele.val)) or <err> in set ranges
then <err>
else let rngs = if range = nil
then {mk_Floatrng(-(beta ** maxint),beta ** maxint)}
else {mk_Floatrng(min(r),max(r)) | r in set ranges} in
mk_Float(rngs, abse.val.val,rele.val.val,{});
eval_StrucRep : StrucRep -> Env -> (Expressible_type | Errvalue)
eval_StrucRep(mk_StrucRep(reps))(e) ==
let tps = [ eval_Representation(r)(e) | r in seq reps] in
if exists tp in seq tps & not(is_TrType(tp) or is_Float(tp) or
is_IntType(tp))
then <err>
elseif exists tp1,tp2 in seq tps & fleq(tp1,tp2)
then <err>
else mk_StructureType(tps,{});
eval_VecRep : VecRep -> Env -> (Expressible_type | Errvalue)
eval_VecRep(mk_VecRep(range,rep))(e) ==
let nrange = eval_Range(range)(e),
type = eval_Representation(rep)(e) in
if type = <err> or nrange = <err>
then <err>
else mk_VectorType(min(nrange),max(nrange),type,{});
eval_UnionRep : UnionRep -> Env -> (Expressible_type | Errvalue)
eval_UnionRep(mk_UnionRep(reps))(e) ==
let tps = {eval_Representation(rep)(e) | rep in seq reps} in
if exists tp in set tps & not (is_IntType(tp) or is_Float(tp) or
is_TrType(tp) or is_VoidType(tp))
then <err>
elseif exists tp1,tp2 in set tps & fleq(tp1,tp2)
then <err>
else mk_UnionType(tps,{});
eval_FlavouredRep : FlavouredRep -> Env -> (Expressible_type | Errvalue)
eval_FlavouredRep(mk_FlavouredRep(fl,rep))(e) ==
let type = eval_Representation(rep)(e),
flav = eval_Flavouring(fl) in
if type = <err>
then <err>
else replace_flavour(type,flav);
eval_TypeDec : TypeDec -> EnvState -> EnvState
eval_TypeDec(mk_TypeDec(id,tp))(mk_(e,ps)) ==
let type = eval_Type(tp)(e) in
if type = <err>
then <err>
else mk_(update_env(id)(type)(e),ps);
eval_PackageScope : PackageScope -> Env -> PState -> EST_value
eval_PackageScope(mk_PackageScope(ids,decls,expr))(mk_(m,l))(ps) ==
let env_st = mk_(mk_(m,l),ps) in
let new_env_st = eval_Decls(decls)(env_st) in
if new_env_st = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else let mk_(mk_(nm,nl),nps) = new_env_st in
if not (elems ids subset (dom nm \ dom m))
then mk_EST_value(<err>,ps.sto,zerot)
else let ne = mk_(((elems ids) union dom m) <: nm, nl) in
eval_Expression(expr)(ne)(nps);
eval_GuardedScope : GuardedScope -> Env -> PState -> EST_value
eval_GuardedScope(mk_GuardedScope(decls,incl,outcl))(e)(ps) ==
let g_decl = eval_GuardedDeclarations(decls)(true)(e)(ps) in
if g_decl = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else let mk_(ne,nps,val) = g_decl in
let in_val = eval_Sequence(incl)(ne)(nps),
out_val = eval_Sequence(outcl)(ne)(nps) in
if in_val.val = <err> or out_val.val = <err>
then mk_EST_value(<err>,ps.sto, zerot)
else let type = setlub({in_val.val.type,out_val.val.type}) in
if type = <err>
then mk_EST_value(<err>,ps.sto, zerot)
else if val
then mk_EST_value(widen_type(in_val.val,type),in_val.sto,
tplus(in_val.time,t_if))
else mk_EST_value(widen_type(out_val.val,type),out_val.sto,
tplus(out_val.time,t_if));
eval_GuardedDeclarations : seq1 of GuardedDeclaration -> bool -> Env
-> PState -> ((Env * PState * bool) | Errvalue)
eval_GuardedDeclarations(decls)(b)(e)(ps) ==
let gdcl = eval_GuardedDecl(hd decls)(e)(ps) in
if len decls = 1
then gdcl
elseif gdcl = <err>
then <err>
else let mk_(ne,nps,tr) = gdcl in
eval_GuardedDeclarations(tl decls)(b and tr)(ne)(nps);
eval_GuardedDecl : GuardedDeclaration -> Env -> PState -> ((Env *
PState * bool) | Errvalue)
eval_GuardedDecl(decl)(e)(ps) ==
if is_WhereDecl(decl)
then eval_WhereDecl(decl)(e)(ps)
else let d = eval_Declaration(decl)(mk_(e,ps)) in
if d = <err>
then <err>
else let mk_(ne,nps) = d in
mk_(ne,nps,true);
eval_WhereDecl : WhereDecl -> Env -> PState -> ((Env * PState * bool) | Errvalue)
eval_WhereDecl(mk_WhereDecl(type,expr,id))(e)(ps) ==
let x = eval_Expression(expr)(e)(ps) in
if x.val = <err>
then <err>
else let t = eval_SkeletonType(type)(x.val.type)(e) in
cases t:
<err> -> <err>,
others -> let env = if id = nil
then e
else update_env(id)(x.val)(e) in
let xt = const_type(x.val) in
cases xt:
<err> -> <err>,
others -> let val = gt(t,xt) in
mk_(env, mk_PState(ps.sto,x.time),val)
end
end;
eval_Assertion : Assertion -> Env -> PState -> EST_value
eval_Assertion(mk_Assertion(expr,tp))(e)(ps) ==
let x = eval_Expression(expr)(e)(ps) in
if x.val = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else let type = eval_SkeletonType(tp)(x.val.type)(e) in
if type = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else let xt = const_type(x.val) in
cases xt:
<err> -> mk_EST_value(<err>,ps.sto,zerot),
others ->
if not (tleq(type,x.val.type) and tleq(xt,type))
then mk_EST_value(<err>,ps.sto,zerot)
else let val = widen_type(x.val, phi_remove(type)) in
mk_EST_value(val,x.sto,tplus(x.time,t_widen_type))
end;
eval_Conditional: Conditional -> Env -> PState -> EST_value
eval_Conditional(mk_Conditional(cond))(e)(ps) ==
if is_IfThenOnly(cond)
then eval_IfThenOnly(cond)(e)(ps)
elseif is_IfThenElse(cond)
then eval_IfThenElse(cond)(e)(ps)
else eval_CaseExpr(cond)(e)(ps);
eval_IfThenOnly : IfThenOnly -> Env -> PState -> EST_value
eval_IfThenOnly(mk_IfThenOnly(prop,action))(e)(ps) ==
let cond = eval_Expression(prop)(e)(ps),
aseq = eval_Sequence(action)(e)(mu(ps,time |-> tplus(cond.time,t_if)))
in
if not is_Tr(cond.val) or not is_Void(aseq.val)
then mk_EST_value(<err>,ps.sto,zerot)
elseif cond.val.val
then aseq
else mk_EST_value(mk_Void(<nil>,mk_VoidType({})),ps.sto,
tplus(ps.time,tplus(cond.time,t_if)));
eval_IfThenElse : IfThenElse -> Env -> PState -> EST_value
eval_IfThenElse(mk_IfThenElse(prop,thenaction,elseaction))(e)(ps) ==
let cond = eval_Expression(prop)(e)(ps) in
if not is_Tr(cond.val)
then mk_EST_value(<err>,ps.sto,zerot)
else let then_x = eval_Sequence(thenaction)(e)(ps),
else_x = eval_Sequence(elseaction)(e)(ps) in
let type = lub(then_x.val.type,else_x.val.type) in
if type = <err>
then mk_EST_value(<err>,ps.sto,zerot)
elseif cond.val.val
then mu(then_x, val |-> widen_type(then_x.val,type),
time |-> tplus(then_x.time,cond.time))
else mu(else_x, val |-> widen_type(else_x.val,type),
time |-> tplus(else_x.time,cond.time));
eval_CaseExpr : CaseExpr -> Env -> PState -> EST_value
eval_CaseExpr(mk_CaseExpr(expr,limbs,outlimb))(e)(ps) ==
let x = eval_Expression(expr)(e)(ps) in
if x.val = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else let type_x = x.val.type in
let ls = eval_Limbs(limbs)(x.val)(e)(mu(ps,time |-> x.time)) in
let os = if outlimb = nil
then []
else let mk_(t,v) = ls(len ls) in
[mk_(type_x,eval_Sequence(outlimb)(e)(mu(ps,time
|-> v.time)))] in
let pats = ls^os in
if exists mk_(t,v) in seq pats & v.val = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else let patlub = setlub({t | mk_(t,v) in seq pats}) in
if patlub = <err>
then mk_EST_value(<err>,ps.sto,zerot)
elseif lub(type_x,patlub) <> patlub
then mk_EST_value(<err>,ps.sto,zerot)
else let type = setlub({v.val.type | mk_(t,v) in seq pats}) in
if type = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else let x_type = const_type(x.val) in
let matches = [p | p in seq pats &
let mk_(t,v) = p in
lub(x_type,t) = t] in
let mk_(mt,mv) = hd matches in
let time =
dtplus([mv.time,t_const_type,t_widen_type]) in
mk_EST_value(widen_type(mv.val,type),mv.sto,time);
eval_Limbs : seq1 of CaseLimb -> Expressible_value -> Env -> PState ->
seq1 of (Expressible_type * EST_value)
eval_Limbs(limbs)(x)(e)(ps) ==
let mk_(t,v) = eval_Limb(hd limbs)(x)(e)(ps) in
if len limbs = 1
then [mk_(t,v)]
else [mk_(t,v)]^(eval_Limbs(tl limbs)(x)(e)(mu(ps,time |-> v.time)));
eval_Limb : CaseLimb -> Expressible_value -> Env -> PState ->
(Expressible_type * EST_value)
eval_Limb(mk_CaseLimb(test,sequ))(x)(e)(ps) ==
let t = eval_Tester(test)(x)(e)(ps) in
if t = <err>
then mk_(mk_VoidType({}),mk_EST_value(<err>,ps.sto,zerot))
else let mk_(type,env,tm) = t in
let val = eval_Sequence(sequ)(env)(mu(ps,time |-> tm)) in
if val.val = <err>
then mk_(mk_VoidType({}),mk_EST_value(<err>,ps.sto,zerot))
else mk_(type,val);
eval_Tester : Tester -> Expressible_value -> Env -> PState ->
((Expressible_type * Env * Time) | Errvalue)
eval_Tester(tester)(x)(e)(ps) ==
cases tester:
mk_SkeletonType(t) ->
let nt = eval_SkeletonType(tester)(x.type)(e) in
if nt = <err>
then <err>
else mk_(nt,e,ps.time),
mk_StrucTest(s) -> eval_StrucTest(tester)(x)(e)(ps),
mk_NonStrucTest(id,tp,fl) -> eval_NonStrucTest(tester)(x)(e)(ps)
end;
eval_SkeletonType : SkeletonType -> Expressible_type -> Env ->
(Expressible_type | Errvalue)
eval_SkeletonType(mk_SkeletonType(skel))(t)(e) ==
cases skel:
mk_Type(t) -> eval_Type(skel)(e),
mk_NumSkel(r,er) -> eval_NumSkel(skel)(t)(e),
mk_StrucSkel(s) -> eval_StrucSkel(skel)(t)(e),
mk_FlavSkel(s,fl) -> eval_FlavSkel(skel)(t)(e),
mk_VecSkel(s) -> eval_VecSkel(skel)(t)(e),
mk_UnionSkel(s) -> eval_UnionSkel(skel)(t)(e)
end;
eval_NumSkel : NumSkel -> Expressible_type -> Env ->
(Expressible_type | Errvalue)
eval_NumSkel(mk_NumSkel(ranges,errors))(x_type)(e) ==
if not (is_TrType(x_type) or is_IntType(x_type) or is_Float(x_type))
then <err>
else let rngs = if ranges = nil
then if is_Float(x_type)
then {{l,...,u} | mk_Floatrng(l,u) in set x_type.range}
else {x_type.range}
else {eval_Range(r)(e) | r in seq ranges} in
if <err> in set rngs
then <err>
else cases x_type:
mk_TrType(range,fl) ->
if not (dunion rngs subset {0,1})
then <err>
else mk_TrType({{0 |->false, 1 |->
true}(v) | v in set dunion rngs},fl),
mk_IntType(rep,range,fl) ->
if (rep = <byte> and exists v in set dunion rngs &
abs v >= bytemax) or
(exists v in set dunion rngs & abs v >= maxint)
then <err>
else mk_IntType(rep,dunion rngs,fl),
mk_Float(rs,abse,rele,fl) ->
if exists v in set dunion rngs & abs v >= maxint
then <err>
else
let abserr
= if errors.abserr = nil
then abse
else
let v1 =
(eval_CompileTimeValue(errors.abserr)(e)).val in
if v1 = <err>
then <err>
else v1.val,
relerr
= if errors.relerr = nil
then rele
else
let v1 =
(eval_CompileTimeValue(errors.relerr)(e)).val in
if v1 = <err>
then <err>
else v1.val in
if not (is_real(abserr) and is_real(relerr))
then <err>
else mk_Float({mk_Floatrng(min(r),max(r))
| r in set rngs},abserr,relerr,fl)
end;
eval_StrucSkel : StrucSkel -> Expressible_type -> Env ->
(Expressible_type | Errvalue)
eval_StrucSkel(mk_StrucSkel(comps))(x_type)(e) ==
if not is_StructureType(x_type)
then <err>
elseif struc_length(x_type) <> len comps
then <err>
else let t = [if comps(i) = <nil>
then x_type.tps(i)
else eval_SkeletonType(comps(i))(x_type.tps(i))(e) |
i in set inds comps] in
if exists tp in seq t & not (is_TrType(tp) or
is_IntType(tp) or is_Float(tp))
then <err>
else mk_StructureType(t,x_type.fl);
eval_FlavSkel : FlavSkel -> Expressible_type -> Env ->
(Expressible_type | Errvalue)
eval_FlavSkel(mk_FlavSkel(skel,fl))(x_type)(e) ==
let t = eval_SkeletonType(skel)(x_type)(e),
f = eval_Flavouring(fl) in
if t = <err>
then <err>
else replace_flavour(t,f);
eval_VecSkel : VecSkel -> Expressible_type -> Env ->
(Expressible_type | Errvalue)
eval_VecSkel(mk_VecSkel(skel))(x_type)(e) ==
let t = eval_SkeletonType(skel)(x_type)(e) in
if t = <err>
then <err>
else cases x_type:
mk_VectorType(l,u,tp,fl) -> mk_VectorType(l,u,t,fl),
others -> <err>
end;
eval_UnionSkel : UnionSkel -> Expressible_type -> Env ->
(Expressible_type | Errvalue)
eval_UnionSkel(mk_UnionSkel(skels))(x_type)(e) ==
let fls = { skel |-> fl | skel in seq skels, fl : Flavdom &
fl = cases skel:
mk_FlavSkel(skel,f) -> eval_Flavouring(f),
mk_FlavouredType(f,t) -> eval_Flavouring(f),
others -> eval_Flavouring(skel)
end} in
if card dom fls <> card rng fls
then <err>
elseif is_UnionType(x_type)
then let x_fls = merge{
{ mk_VoidType(f) |-> f | mk_VoidType(f) in set x_type.tps},
{ mk_IntType(rep,range,fl) |-> fl |
mk_IntType(rep,range,fl) in set x_type.tps },
{ mk_TrType(range,fl) |-> fl |
mk_TrType(range,fl) in set x_type.tps },
{ mk_Float(rs,a,r,fl) |-> fl |
mk_Float(rs,a,r,fl) in set x_type.tps }}
in
if not (rng fls subset rng x_fls)
then <err>
else let tps =
{ cases skel:
mk_FlavSkel(s,f) -> eval_FlavSkel(skel)(tp)(e),
mk_FlavouredType(f,t) -> eval_FlavouredType(skel)(e),
others -> eval_VoidValType(skel)(e)
end | skel in seq skels, tp in set x_type.tps &
fls(skel) = x_fls(tp)} in
if exists tp in set tps & not (is_TrType(tp) or is_IntType(tp)
or is_Float(tp) or is_VoidType(tp))
then <err>
else mk_UnionType(tps,x_type.fl)
else let fl = if is_VoidType(x_type)
then x_type
else x_type.fl in
if fl not in set rng fls
then <err>
else let skel = iota s in set elems skels & fls(s) = fl in
cases skel:
mk_FlavSkel(s,f) -> eval_FlavSkel(skel)(x_type)(e),
mk_FlavouredType(f,t) -> eval_FlavouredType(skel)(e),
others -> eval_VoidValType(skel)(e)
end;
eval_NonStrucTest : NonStrucTest -> Expressible_value -> Env -> PState
-> ((Expressible_type * Env * Time) | Errvalue)
eval_NonStrucTest(mk_NonStrucTest(id,fl,skel))(x)(e)(ps) ==
let t = eval_SkeletonType(skel)(x.type)(e) in
if t = <err>
then <err>
else let t' = if fl = nil
then t
else replace_flavour(t,eval_Flavouring(fl)) in
if id = nil
then mk_(t',e,ps.time)
else mk_(t',update_env(id)(x)(e), ps.time);
eval_StrucTest : StrucTest -> Expressible_value -> Env -> PState ->
((Expressible_type * Env * Time) | Errvalue)
eval_StrucTest(mk_StrucTest(tests))(x)(e)(ps) ==
if not is_Structure(x)
then <err>
elseif struc_length(x.type) <> len tests
then <err>
else let xs = [ construct_ev(x.val(i),x.type.tps(i)) | i in set inds
x.val] in
let ts = eval_Testseq(tests)(xs)(e)(ps) in
if ts = <err>
then <err>
else let mk_(tps,env,time) = ts in
mk_(mk_StructureType(tps,x.type.fl),env,time);
eval_Testseq : seq of (NonStrucTest | <nil>) -> seq of Expressible_value
-> Env -> PState -> ((seq of Expressible_type * Env
* Time) | Errvalue)
eval_Testseq(tests)(xs)(e)(ps) ==
if tests = []
then mk_([],e,ps.time)
else let t = if hd tests = <nil>
then mk_((hd xs).type, e, ps.time)
else eval_NonStrucTest(hd tests)(hd xs)(e)(ps) in
if t = <err>
then <err>
else let mk_(tp,env,time) = t in
let ts = eval_Testseq(tl tests)(tl xs) (env) (mu(ps,time |-> time))
in
if ts = <err>
then <err>
else let mk_(tps,n_env,n_time) = ts in
mk_([tp]^tps,n_env,n_time);
eval_OuterLoop : OuterLoop -> Env -> PState -> EST_value
eval_OuterLoop(mk_OuterLoop(oul))(e)(ps) ==
if is_OuterIntLoop(oul)
then eval_OuterIntLoop(oul)(e)(ps)
else eval_OuterVecLoop(oul)(e)(ps);
eval_OuterIntLoop : OuterIntLoop -> Env -> PState -> EST_value
eval_OuterIntLoop(mk_OuterIntLoop(mk_OverRange(id,range),actns))(e)(ps) ==
let nrange = eval_Range(range)(e) in
if nrange = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else let vec_elems = [eval_Sequence(actns)(update_env(id)
(mk_Storable_value(mk_Int(i,mk_IntType(<word>,{i},{}))))(e))
(mu(ps,time |-> zerot)) | i in set nrange] in
if <err> in set {x.val | x in seq vec_elems}
then mk_EST_value(<err>,ps.sto,zerot)
else let type = seqlub([i.val.type | i in seq vec_elems]),
time = dtplus([i.time | i in seq vec_elems]) in
if type = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else let vec_val = if is_StructureType(type) or
is_VectorType(type)
then [ v.val.val | v in seq vec_elems]
else [ v.val | v in seq vec_elems] in
mk_EST_value(mk_Vector(vec_val,mk_VectorType(1,len
vec_val,type,{})),ps.sto, tplus(ps.time,time));
eval_OuterVecLoop : OuterVecLoop -> Env -> PState -> EST_value
eval_OuterVecLoop(mk_OuterVecLoop(ovs,actions))(e)(ps) ==
let idvs = eval_OverVectors(ovs)(e)(ps) in
if idvs = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else let time1 = dtplus([ let mk_(id,v,t) = i in t | i in seq idvs]),
new_env = lambda i:nat &
(multi_update_env([ let mk_(id,v,t) = j in
mk_(id,vector_extract(v,i)) |
j in seq idvs]^(
if ovs.cnt = nil then []
else [mk_(ovs.cnt,i)]))(e)) in
let vec_elems = [eval_Sequence(actions)(new_env(i))(mu(ps,time
|-> zerot)) | i in set let mk_(i1,v,t) =
idvs(1) in inds (v.val)] in
if <err> in set {x.val | x in seq vec_elems}
then mk_EST_value(<err>,ps.sto,zerot)
else let type = seqlub([i.val.type | i in seq vec_elems]),
time = dtplus([i.time | i in seq vec_elems]^[time1]) in
if type = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else let new_tp = mk_VectorType(1,len vec_elems,type,{}) in
let vec_val = if is_StructureType(type) or
is_VectorType(type)
then [i.val.val | i in seq vec_elems]
else [i.val | i in seq vec_elems] in
let new_vec = mk_Vector(vec_val,new_tp) in
mk_EST_value(new_vec,ps.sto,tplus(ps.time,time));
eval_OverVectors : OverVectors -> Env -> PState -> (seq1 of (Id * Vector *
Time) | Errvalue)
eval_OverVectors(ovs)(e)(ps) ==
let indices = [ let mk_OverVector(id,val) = o in
let x = eval_Operation(val)(e)(mu(ps,time |-> zerot)) in
mk_(id,x.val,x.time) | o in seq ovs.ovv] in
if exists i in set inds indices & let mk_(id,v,t) = indices(i) in
not is_Vector(v)
then <err>
else indices;
eval_InnerLoop : InnerLoop -> Env -> PState -> EST_value
eval_InnerLoop(mk_InnerLoop(innerl))(e)(ps) ==
cases innerl:
mk_IntLoop(inc,actions) -> eval_IntLoop(innerl)(e)(ps),
mk_VecLoop(ovs,actions) -> eval_VecLoop(innerl)(e)(ps),
mk_TimeLoop(time,actions) -> eval_TimeLoop(innerl)(e)(ps)
end;
eval_IntLoop : IntLoop -> Env -> PState -> EST_value
eval_IntLoop(mk_IntLoop(inc,actions))(e)(ps) ==
let idrng = eval_InnerControl(inc)(e)(ps) in
if idrng = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else let mk_(id,range) = idrng in
let f: EST_Iterate -> EST_Iterate
= lambda x: EST_Iterate &
let new_env = update_env(id)(
mk_Storable_value(mk_Int(range(x.i),
mk_IntType(<word>,elems range,{}))))(e) in
eval_SeqIterate(actions)(new_env)(x) in
let exi = (NIterate(f,(len range)))(mk_EST_Iterate(
mk_EST_value(mk_Void(<nil>,mk_VoidType({})), ps.sto,ps.time),1)) in
exi.expst;
eval_InnerControl : InnerControl -> Env -> PState -> ((Id * seq of
int) | Errvalue)
eval_InnerControl(inc)(e)(ps) ==
cases inc:
mk_OverRange(cnt,range) ->
let r = eval_Range(range)(e) in
if r = <err> then <err> else mk_(cnt,[x | x in set r]),
mk_PartialRange(cnt,from_b,to_b,inc) ->
let b1 = eval_Operation(from_b)(e)(ps),
b2 = eval_Operation(to_b)(e)(ps) in
if not (is_Int(b1.val) and is_Int(b2.val))
then <err>
else let b3 = if inc = nil
then if b1.val.val <= b2.val.val
then mk_Int(1,mk_IntType(<byte>,{1,-1},{}))
else mk_Int(-1,mk_IntType(<byte>,{1,-1},{}))
else (eval_Operation(inc)(e)(ps)).val in
if not (is_Int(b3.val)) or
(is_Int(b3.val) and
exists v1 in set b1.val.type.range,
v2 in set b2.val.type.range,
v3 in set b3.val.type.range & (v2-v1)*v3 < 0)
then <err>
else let r = [ b1.val.val + alpha * b3.val | alpha in set
{0,...,floor(1+(b2.val.val-b1.val.val)/b3.val)} &
abs (alpha * b3.val) <= abs (b2.val.val - b1.val.val)] in
mk_(cnt,r)
end;
eval_SeqIterate : Sequence -> Env -> EST_Iterate -> EST_Iterate
eval_SeqIterate(sequ)(e)(exi) ==
if exi.expst.val = <err>
then mu(exi, i |-> exi.i + 1)
else let new_expst = eval_Sequence(sequ)(e)(mk_PState(exi.expst.sto,exi.expst.time)) in
mk_EST_Iterate(new_expst,exi.i + 1);
eval_VecLoop : VecLoop -> Env -> PState -> EST_value
eval_VecLoop(mk_VecLoop(ovs,actions))(e)(ps) ==
let indices = eval_OverVectors(ovs)(e)(ps) in
if indices = <err>
then mk_EST_value(<err>,ps.sto,zerot)
else let time = dtplus([let mk_(id,v,t) = i in t | i in seq indices]) in
let f:EST_Iterate -> EST_Iterate
= lambda x:EST_Iterate &
let env = multi_update_env(
[let mk_(id,v,t) = indices(i) in
mk_(id,vector_extract(v,x.i)) |i in set inds indices])(e),
new_expst = mu(x.expst, time |-> x.expst.time)
in
let new_env = if ovs.cnt = nil then env
else update_env(ovs.cnt)
(mk_Storable_value(mk_Int(x.i,mk_IntType(<word>,{x.i},{}))))(env) in
eval_SeqIterate(actions)(new_env)(mu(x,expst |-> new_expst)) in
let mk_(-,v,-) = indices(1) in
let exi = (NIterate(f,len v.val))(mk_EST_Iterate(mk_EST_value(
mk_Void(<nil>,mk_VoidType({})),
ps.sto,tplus(ps.time,time)),1))
in
exi.expst;
eval_TimeLoop : TimeLoop -> Env -> PState -> EST_value
eval_TimeLoop(mk_TimeLoop(time,actions))(e)(ps) ==
let t = eval_TimeInterval(time)(e),
x = eval_Sequence(actions)(e)(mu(ps,time |-> zerot)) in
if t = <err> or x.val = <err>
then mk_EST_value(<err>,ps.sto,zerot)
elseif exists n:nat & timeleq(dtplus([x.time | i in set {1,...,n}]),t)
then let its = iota n:nat &
timeleq(dtplus([x.time | i in set {1,...,n}]),t) and
not (timeleq(dtplus([x.time | i in set {1,...,n+1}]),t)),
f:EST_value ->EST_value = lambda exs:EST_value &
eval_Sequence(actions)(e)(mk_PState(exs.sto,exs.time)) in
(Iterate(f,its))(mk_EST_value(mk_Void(<nil>,mk_VoidType({})),
ps.sto,ps.time))
else mk_EST_value(<err>,ps.sto,zerot);
eval_Assignment : Assignment -> Env -> PState -> EST_value
eval_Assignment(mk_Assignment(ass))(env)(ps) ==
cases ass:
mk_NvAssignment(d,e) -> eval_NvAssignment(ass)(env)(ps),
mk_MultAssignment(d,m,e) -> eval_MultAssignment(ass)(env)(ps),
mk_StrAssignment(d,e) -> eval_StrAssignment(ass)(env)(ps)
end;
eval_NvAssignment : NvAssignment -> Env -> PState -> EST_value
eval_NvAssignment(mk_NvAssignment(dest,expr))(e)(ps) ==
let l = access_env(dest)(e) in
if not is_Location(l)
then mk_EST_value(<err>,ps.sto,zerot)
else let x = eval_Expression(expr)(e)(ps) in
if x.val = <err>
then mk_EST_value(<err>,ps.sto,zerot)
elseif cases x.val.type:
mk_VoidType(t) -> t = {Phi},
others -> x.val.type.fl = {Phi}
end
then mk_EST_value(<err>,ps.sto,zerot)
else let mk_Storable_value(dest_val) = access(l)(ps.sto) in
if gt(dest_val.type,x.val.type)
then let new_sto =
update(l)(mk_Storable_value(widen_type(x.val,dest_val.type)))(ps.sto) in
mk_EST_value(mk_Void(<nil>,mk_VoidType({})),new_sto,
tplus(tplus(ps.time,t_update),t_access))
else mk_EST_value(<err>,ps.sto,zerot);
eval_MultAssignment : MultAssignment -> Env -> PState -> EST_value
eval_MultAssignment(mk_MultAssignment(dest,mult,expr))(e)(ps) ==
let l = access_env(dest)(e) in
if not is_Location(l)
then mk_EST_value(<err>,ps.sto,zerot)
else let mk_Storable_value(v) = access(l)(ps.sto) in
if not is_Vector(v)
then mk_EST_value(<err>,ps.sto,zerot)
else let mk_Vector(val,type) = v in
let v' =
eval_VectorMult(mk_EST_value(v,ps.sto,ps.time))(mult)(e) in
let x = eval_Expression(expr)(e)(mk_PState(v'.sto,v'.time)) in
if v'.val = <err> or not is_Vector(x.val)
then mk_EST_value(<err>,ps.sto,zerot)
elseif (x.val.type.upper - x.val.type.lower) <>
(v'.val.type.upper - v'.val.type.lower) or
not gt(v.type.type,x.val.type.type) or
cases x.val.type.type:
mk_VoidType(t) -> t = {Phi},
others -> x.val.type.fl = {Phi}
end
then mk_EST_value(<err>,ps.sto,zerot)
else let vleft = mk_Vector(vector_subv(val,type.lower,
v'.val.type.lower-1),mk_VectorType(type.lower,
v'.val.type.lower-1,type.type,type.fl)),
vmid = x.val,
vright = mk_Vector(vector_subv(val,v'.val.type.upper+1,
type.upper),mk_VectorType(v'.val.type.upper+1,
type.upper,type.type, type.fl)) in
let new_vec = vector_concat(vector_concat(vleft,vmid),vright),
new_time = dtplus([x.time,t_vector_concat,
t_vector_concat, vector_subv,vector_subv]) in
mk_EST_value(mk_Void(<nil>,mk_VoidType({})),
update(l)(mk_Storable_value(new_vec))(ps.sto),
new_time);
eval_StrAssignment : StrAssignment -> Env -> PState -> EST_value
eval_StrAssignment(mk_StrAssignment(dest,expr))(e)(ps) ==
let ls = [access_env(d)(e) | d in seq dest] in
if exists l in seq ls & not is_Location(l)
then mk_EST_value(<err>,ps.sto,zerot)
else let x = eval_Expression(expr)(e)(ps) in
if not is_Structure(x.val)
then mk_EST_value(<err>,ps.sto,zerot)
elseif len ls <> struc_length(x.val.type)
then mk_EST_value(<err>,ps.sto,zerot)
else let nvals = [ access(l)(ps.sto) | l in seq ls] in
let vals = [ let mk_Storable_value(v) = i in v | i in seq nvals] in
let dest_tps = [v.type | v in seq vals],
x_tps = [i | i in seq x.val.type.tps] in
if exists i in set inds dest_tps & not gt(dest_tps(i),x_tps(i))
then mk_EST_value(<err>,ps.sto,zerot)
else let ys = [mk_Storable_value(construct_ev(x.val.val(i),
x.val.type.tps(i))) | i in set inds x.val.val],
new_t = dtplus([x.time,t_access,t_construct_ev,
t_multi_update(len ys)]) in
mk_EST_value(mk_Void(<nil>,mk_VoidType({})),
multi_update(ls)(ys)(ps.sto), new_t);
eval_TimedExpression : TimedExpression -> Env -> PState -> EST_value
eval_TimedExpression(mk_TimedExpression(texpr))(e)(ps) ==
if is_TimeTakes(texpr)
then eval_TimeTakes(texpr)(e)(ps)
else eval_TimeAssertion(texpr)(e)(ps);
eval_TimeTakes : TimeTakes -> Env -> PState -> EST_value
eval_TimeTakes(mk_TimeTakes(expr,time))(e)(ps) ==
let x = eval_Expression(expr)(e)(mu(ps, time |-> zerot)),
t = eval_TimeInterval(time)(e) in
if x.val = <err> or t = <err>
then mk_EST_value(<err>,ps.sto,zerot)
elseif timeleq(x.time,t)
then mu(x,time |-> tplus(ps.time,x.time))
else mk_EST_value(<err>,ps.sto,zerot);
eval_TimeInterval : TimeInterval -> Env -> (Time | Errvalue)
eval_TimeInterval(time)(e) ==
let range = eval_Range(time)(e) in
if range = <err> or min(range) < 0
then <err>
else mk_(min(range),max(range));
eval_TimeAssertion:TimeAssertion -> Env -> PState -> EST_value
eval_TimeAssertion(mk_TimeAssertion(expr,time))(e)(ps) ==
let x = eval_Expression(expr)(e)(mu(ps, time |-> zerot)),
t = eval_TimeInterval(time)(e) in
if x.val = <err> or t = <err>
then mk_EST_value(<err>,ps.sto,zerot)
elseif timeleq(t,x.time)
then mu(x,time |-> tplus(ps.time,t))
else mk_EST_value(<err>,ps.sto,zerot);
Iterate: (EST_value -> EST_value) * nat -> (EST_value ->
EST_value)
Iterate(f,n) ==
if n = 0
then lambda x:EST_value & x
elseif n = 1
then f
else f comp (Iterate( f, n-1));
NIterate: (EST_Iterate -> EST_Iterate) * nat -> (EST_Iterate ->
EST_Iterate)
NIterate(f,n) ==
if n = 0
then lambda x:EST_Iterate & x
elseif n = 1
then f
else f comp (NIterate( f, n-1))