fact: Definition Postcondition (p : Program) (c : Class) (m : Method) (st : State.t) : Prop := let st' := pre_state m st in ( match METHOD.kind m , st@fr@this with | Constructor, Some loc => (forall o : Object, EvalObjectInvariant p m o st) /\ EvalInitially p c m st | Finalizer, Some loc => forall o : Object, o <> loc -> EvalObjectInvariant p m o st | _ , _ => forall o : Object, EvalObjectInvariant p m o st end ) /\ forall c', EvalStaticInvariant p c' m st /\ (forall sc , DefinedCase c m sc -> match Frame.ret st@fr with | Normal _ => EvalRequires p m sc st' -> EvalEnsures p m sc st | Exception _ => EvalRequires p m sc st' -> ( EvalSignals p m sc st /\ EvalSignalsOnly p sc st ) end ).
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)