fact: Fixpoint EvalBoolExpression (e : Expression) (st : State.t) {struct e} : Prop := match e with | var _ | quantifier _ | param _ | field _ _ | modelField _ _ | method _ _ _ | \result => v2b $ EvalExpression EvalBoolExpression EvalRefExpression EvalNumExpression e st | literal (BoolLiteral b) => b | UnaryBoolExpr op e => EvalUnaryBoolOp op (EvalBoolExpression e st) | BinaryBoolExpr op e1 e2 => EvalBinaryBoolOp op (EvalBoolExpression e1 st) (EvalBoolExpression e2 st) | BinaryCondBoolExpr op e1 e2 => EvalBinaryCondBoolOp EvalBoolExpression op e1 e2 st | RelationalExpr op e1 e2 => EvalRelationalOp op (EvalNumExpression e1 st) (EvalNumExpression e2 st) | BinaryRefExpr op e1 e2 => EvalBinaryRefOp op (EvalRefExpression e1 st) (EvalRefExpression e2 st) | JMLBinaryBoolExpr op e1 e2 => EvalJMLBoolOp op (EvalBoolExpression e1 st) (EvalBoolExpression e2 st) | Conditional cond t e => EvalBoolConditional EvalBoolExpression cond t e st | e1 <: e2 => types_compatible p (EvalType EvalRefExpression e1 st) (EvalType EvalRefExpression e2 st) | e instanceof t => EvalInstanceof EvalRefExpression e t st | \old e => EvalBoolExpression e (pre_state m st) | \fresh flist => EvalFresh EvalRefExpression flist st | \nonnullelements e => EvalNonnullElements EvalRefExpression e st | \forall1 qvar ; r ; e => forall v , EvalQuantifier EvalBoolExpression qvar r e v st | \exists1 qvar ; r ; e => exists v , EvalQuantifier EvalBoolExpression qvar r e v st | _ => UndefinedProp end with EvalRefExpression (e : Expression) (st : State.t) {struct e} : option Object := match e with | var _ | quantifier _ | param _ | field _ _ | modelField _ _ | method _ _ _ | \result => v2l $ EvalExpression EvalBoolExpression EvalRefExpression EvalNumExpression e st | null => None | this => v2l $ ParamDict.get (Frame.params st@fr) paramThis | Cast t e => EvalRefExpression e st | \old e => EvalRefExpression e (pre_state m st) | new t => EvalNewExpression t st | _ => None end with EvalNumExpression (e : Expression) (st : State.t) {struct e} : num := match e with | var _ | quantifier _ | param _ | field _ _ | modelField _ _ | method _ _ _ | \result => v2n $ EvalExpression EvalBoolExpression EvalRefExpression EvalNumExpression e st | literal (IntLiteral n) => I (Int.const n) | UnaryIntExpr op e => EvalUnaryNumOp op (EvalNumExpression e st) | BinaryIntExpr op e1 e2 => EvalBinaryNumOp op (EvalNumExpression e1 st) (EvalNumExpression e2 st) | Cast t e => EvalNumExpression e st | \old e => EvalNumExpression e (pre_state m st) | Quantification q v r e => I (EvalGeneralizedQuantifier EvalBoolExpression EvalNumExpression q v r e st) | _ => UndefinedNum end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)