Event-B is suitable for various modelling problems, in particular,
sequential program development. A fundamental property to be proved
initially for sequential programs development is feasibility, i.e.
whether the initially specified post-condition is satisfiable under the
stated pre-condition.

There is an "obvious" way of proving feasibility at the beginning of a
sequential program development, because, in Event-B, each event is
associated with a feasibility proof obligation. It would be possible
to use this for proving feasibility of sequential programs. But the
corresponding proof usually requires instantiating an existential
quantifier and this might be sometimes problematic.
 
However, there is a better way of doing it that suits well with
refinement. The algorithm to be constructed is supposed to establish
the post-condition, too. Thus, we can save the initial feasibility
proof by exploiting this fact.

In this presentation, we formally justify this approach and describe a
corresponding refinement method for the development of sequential
programs in Event-B. An example illustrates our approach.