fact: Definition EvalEnsures (sc : SpecificationCase) (st : State.t) : Prop := match ENSURES.pred (CASE.ensures sc) with | (:expr:) => EvalPredicate expr st | \not_specified => NotSpecifiedEnsures end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)