Abstract: The constructive approach to software correctness aims at formal modelling of the intended behaviour and structure of a system in different levels of abstraction and verifying properties of models. The target of analytical approach is to verify properties of the final program code. A high level look at these two approaches suggests that the constructive and analytical approaches should complement each other well. The aim of this thesis is to build a link between Event-B (constructive approach) and Dafny (analytical approach) for developing sequential verified programs. The first contribution of this thesis is a tool supported method for transforming Event-B models to simple Dafny code contracts (in the form of method pre- and post-conditions). Transformation of Event-B formal models to Dafny method declarations and code contracts is enabled by a set of transformation rules. Using this set of transformation rules, one can generate code contracts from Event-B models but not implementations. The generated code contracts must be seen as an interface that can be implemented. If there is an implementation that satisfies the generated contracts then it is considered to be a correct implementation of the abstract Event-B model. A tool for automatic transformation of Event-B models to simple Dafny code contracts is presented. The second contribution of this thesis is an approach for derivation of algorithmic structure in Event-B refinement. To facilitate this, we augment Event-B with a scheduling language that allows modeller to explicitly define the control flow between Event-B events in each refinement level. The scheduling language supports both non …