| products/sources/formale sprachen/VDM/VDMSL/newspeakSL/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: newspeak.vdmsl Sprache: VDMOriginal von: VDM© |
|
||||||
|
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) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
