On 18 March 2013 09:46, Jocelyn Fiat <notifications@github.com> wrote:

> In library/server/wsf/router/wsf_routed_service.e:
>
> > +		require
> > +			unavailable: unavailable = True
> > +			res_attached: res /= Void
> > +		local
> > +			h: HTTP_HEADER
> > +		do
> > +			create h.make
> > +			h.put_content_type_text_plain
> > +			check attached {READABLE_STRING_8} unavailablity_message as m then
> > +					-- invariant
>
> In addition, please avoid to use
>
>
> check ... then
> end
> In new void-safe code .. this should really be avoided as much as possible
> (if not ... always avoided)
>
How can it be avoided here? Is the invariant clause regarded as a CAP? No.
We don't have any CAPs that combine a precondition  with an invariant of
form precondition implies /= Void and deduce  attached.