fact: Definition heavyweightDefaults (spec:FULL_SPEC_CASE.t) (this:METHOD.t) : FullSpecCaseDefaults := let codeContract := FULL_SPEC_CASE.isCodeContract spec in let headerDefault := requiresSH false (: true' :)%jml in let bodyDefault (t0:TAG.tag) := match t0 with | ensuresT => ensuresC false (: true' :)%jml | signalsT => signalsC false (Exception_e, (: true' :)%jml) | signalsOnlyT => signalsOnlyC false (filterCheckedExceptions (METHOD.throws this)) | divergesT => divergesC false (: false' :)%jml | whenT => whenC false (: true' :)%jml | assignableT => assignableC false (: \everything :)%jml | accessibleT => accessibleC false (if codeContract then (: \everything :)%jml else NotSpecified) | callableT => callableC false (if codeContract then (: METHODSPEC.EveryMethod :)%jml else NotSpecified) | measuredByT => measuredByC false (NotSpecified, None) | capturesT => capturesC false (: \everything :)%jml | 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)