fact: Definition normaliseSignals (data:{d:MethodSpecClause | signalsT = TAG.tagOf d}) : MethodSpecClause := let (par, oexpr0) := TAG.mapF signalsT data in let paramType := PARAMSIGNATURE.type (PARAM.signature par) in let oexpr1 := match oexpr0 with | NotSpecified => NotSpecified | Specified expr0 => if isExceptionType paramType then let expr1 := SIGNALS_SUBST.subst par (param Exception_e) expr0 in Specified expr1 else let expr1 := SIGNALS_SUBST.subst par (Cast paramType (param Exception_e)) expr0 in let expr2 := (((param Exception_e) instanceof paramType) ==>' expr1)%jml in Specified expr2 end in signalsC false (Exception_e, oexpr1).
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)