fact: Definition LoopInvariant (p : Program) (c : Class) (m : Method) (pc : PC) (st : State.t) : option Prop := match statement_at m pc with | Some (WhileLoop anno _ _) | Some (DoLoop anno _ _) | Some (ForLoop anno _ _ _ _) => match LOOP_ANNOTATION.expression anno with | (:e:) => Some (EvalPredicate p m e st) | \not_specified => NotSpecifiedLoopInvariant end | _ => None end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)