fact: Definition addDefaults (spec0:FULL_SPEC_CASE.t) (m:METHOD.t) (defaults:FullSpecCaseDefaults) : FULL_SPEC_CASE.t := let (sct,v,r,cc,case0) := spec0 in let (fvd,ovd,sh0,body) := case0 in let clauses0 := match body with | inl cls => cls | inr _ => nil end in let addDefault (tag:ClauseTag) (clauses:list MethodSpecClause) : list MethodSpecClause := match TAG.filterTag tag clauses with | nil => (bodyDefault defaults tag) :: clauses | _ => clauses end in let sh1 := match sh0 with nil => (headerDefault defaults) :: nil | _ => sh0 end in let clauses1 := addDefault durationT clauses0 in let clauses2 := addDefault workingSpaceT clauses1 in let clauses3 := addDefault capturesT clauses2 in let clauses4 := addDefault measuredByT clauses3 in let clauses5 := addDefault callableT clauses4 in let clauses6 := addDefault accessibleT clauses5 in let clauses7 := addDefault assignableT clauses6 in let clauses8 := addDefault whenT clauses7 in let clauses9 := addDefault divergesT clauses8 in let clauses10 := addDefault signalsOnlyT clauses9 in let clauses11 := addDefault signalsT clauses10 in let clauses12 := addDefault ensuresT clauses11 in FULL_SPEC_CASE.Build_t sct v r cc (GENERIC_SPEC_CASE.Build_t fvd ovd sh1 (inl _ clauses12)).
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)