The specification systems of the object-oriented programs with nominative data

Today the problem of fast and economical design of reliable software is up to date. For a quick and economical design of reliable software is possible to apply formal methods of software specifications. Formal methods allow to prove some properties of programs using mathematical methods.
Specifications program should include a description of program goals, functional program structure, input application program output. Problem improving the adequacy of representation of data structures, functions, and compositions used in programming is important.
In this article the notion of abstract computably has been defined. Complete classes of computable functions of various abstraction levels have been described. Formal semantic- syntactic models of specification and programming languages have been defined and investigated.
Imperative and declarative models of nondeterministic programs based on composition- nominative approach are constructed and investigated. Semantics of such programs is presented by partial multi-valued functions. The complete class of naturally computable functions of described type is defined and its algebraic representation is built. A special computability considered in this paper is nominative computability. Nominative computability allows to set adequately a complete class of computable functions over nominative data. At the same time nominative computability is invariant relative to a set of basic elements. Moreover, it is oriented to functions and compositions, which are close to function and compositions of programming languages.
You can increase the adequacy of the default data structures, functions, and compositions used in programming languages if you use nominative data.
Axiomatic theory of nominative data develops a theory of admissible sets. This theory has a number of advantages with respect to the adequacy of programming. It is powerful enough to produce computable function over various data structures. It is not as restrictive as different versions of constructive logic, but not too strong and does not allow, for example, the use of axioms constructing the set of all subsets (compared to the set theory ZF). This theory uses the basic data (praelementy) corresponding methods of constructing data programming.
An axiomatic theory of nominative data, which is capable to specify all computable functions, is constructed. The axiomatic system of program specification over nominative data is constructed.
Prototype axiomatic system software specifications of nominative data (OBJ-NDSL) is constructed. It is based on composition nominative method, axiomatic system software specifications of nominative data and it is based on the sequent calculi for logics. This prototype is based also on language Object-Z.
OBJ-NDSL system allows to prove some properties of programs. shown that for an axiomatic system specification software method can effectively use composition nominative approach. Composition nominative approach is sufficient to adequately meet the needs of programming.