fact: Definition paramNonNullRequires (p:Param) : list SpecHeader := if PARAM.isNullable p || negb (isReferenceType (PARAMSIGNATURE.type (PARAM.signature p))) then nil else requiresSH false (: param p != null :)%jml :: nil.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)