fact: Definition lightweightDefaults (spec:FULL_SPEC_CASE.t) (this:METHOD.t) : FullSpecCaseDefaults := let headerDefault := requiresSH false NotSpecified in let bodyDefault (t0:TAG.tag) : MethodSpecClause := match t0 with | ensuresT => ensuresC false (NotSpecified:optional Expression) | signalsT => signalsC false (Exception_e, NotSpecified) | signalsOnlyT => signalsOnlyC false (filterCheckedExceptions (METHOD.throws this)) | divergesT => divergesC false (: false' :)%jml | whenT => whenC false NotSpecified | assignableT => assignableC false NotSpecified | accessibleT => accessibleC false NotSpecified | callableT => callableC false NotSpecified | measuredByT => measuredByC false (NotSpecified, None) | capturesT => capturesC false NotSpecified | workingSpaceT => workingSpaceC false (NotSpecified, None) | durationT => durationC false (NotSpecified, None) end in Build_FullSpecCaseDefaults headerDefault bodyDefault.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)