Aleksei Alekseev

In this abstract we will describe the principles of tools development for Enterprise Software Development, which reduce developer’s errors. It’s about several practices that are adopted in the department of technological evolution of the our company. These principles will be illustrated by the example of Company Instrumentation for Microsoft .NET.

Maximum static checks. The static checks are checks that are performed during the compilation process. This principle is important, but, unfortunately, often it is underestimated by toolkit developers. Compile-time checks can catch a wide range of errors. There is another feature - a convenience. Runtime errors are harder to perceive and are harder to finding of error cause.

Variety and declarative checks. It’s convenient to specify checks in a declarative form. Moreover, these checks must be implemented by a framework. With duplication reducing and checks declarativity we decrease the probability of error. Checks should be both technical and domain- model level. We will speak about domain-model level.

Ability of analysis and formal verification of declarative checks. Any restrictions generate a certain model. This model can be formally verified. In general, the problem of proving the most of the properties of the program is impossible. This issue goes far beyond the scope of our article. But there is a possibility of verification of the weaker (less expressive models).

We have declarative checks that we call "states". These "states" form a sort of automaton, or the structure of Kripke. So there are algorithms for checking these structures with temporal logics.