fact: Definition addBody (specs0:FULL_SPEC_CASE.t) (clause:MethodSpecClause) : FULL_SPEC_CASE.t := let (sct,v,r,cc,case) := specs0 in let addClause (clauses:list MethodSpecClause) := (clause :: clauses) in let specs1 := FULL_SPEC_CASE.Build_t sct v r cc (clausesMap addClause case) in match sct with | lightweight => specs1 | behaviour => specs1 | normal_behaviour => if isSignalsClause clause then specs0 else specs1 | exceptional_behaviour => if isEnsuresClause clause then specs0 else specs1 end.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)