fact: Definition NewFrame (m : Method) (p : ParamDict.t) (st : State.t) : Frame.t := let adds := FrameAdds.make (LocSet.union st@fr@assignables (ObjSet2LocSet st@fr@fresh)) ObjSet.empty (st@h , p) VarDict.empty in Frame.build m p adds.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)