Liudmyla Omelchuk


In the paper it is developed and grounded the new approaches to building of axiomatic systems of non-determined program specifications. Based on the composition-nominative method of refinement of the concept of program, axiomatic system of software specifications over the nominative data, sequential calculation of the composition-nominative logics and language Object-Z the prototype of axiomatic system of program specifications over nominative data (NDSL++) is built. System NDSL++ allows to prove certain features of the programs. Thus it is demonstrated that the composition-nominative approach can be effectively used for building axiomatic system of program specifications (including object-oriented) over nominative data, which quite adequately meets the problems of programming. 


composition programming; formal method; object-oriented programming; software; verification; system specification

Full Text:



Ambler, Scott W. (2008). The Object Primer: Agile Model Driven Development with UML 2 (3d ed.). Cambridge: Cambridge University Press.

Björner, D., & Henson, M. C. (2008). Logics of Specification Languages. EATCS Monograph in Theoretical Computer Science. Hardcover: Springer.

Booch, G. (2004). Object-oriented Analysis and Design with Applications. Redwood City, Ca.: Addison Wesley Longman Publishing Co., Inc.

Booch, G., Rumbaugh, J. & Jacobsen, I. (1999). The Unified Modeling Language User Guide. Reading. Mass.: Addison-Wesley.

Guttag, J. V., & Horning, J. J. (1993). Larch: Languages and Tools for Formal Specification. Text and Monographs in Computer Science. New York: Springer-Verlag.

Jones, C.B. (1990). Systematic Software Development using VDM (2d ed.), London: Prentice-Hall International.

Nikitchenko, N. (1998). A Composition Nominative Approach to Program Semantics. Techn. Report IT–TR. Technical University of Denmark, Lyngby.

Nikitchenko, N., Omelchuk, L., & Shkilniak S. (2006). Formalisms for Specification of Programs over Nominative Data. Electronic computers and informatics (ECI 2006). Košice, Herl’any, Slovakia, 134-139.

Omelchuk, L. L. (2007). Aksiomatychni systemy specyfikacij program nad nominatyvnymy danymy [Axiomatic Systems of Specifications of Programs over Nominative Data]. Candidate’s thesis. Kyiv [in Ukrainian].

Redko, V. N. (1979). Osnovaniya kompozitsionnogo programmirovaniya [The grounds of the composite programming]. Programmirovanie - Programming, 3, 3–13 [in Russian].

Rodríguez, E., Dwyer, M.B., Flanagan, C., Hatcliff, J., Leavens, G.T. & Robby (2005). Extending JML for modular specification and verification of multi-threaded programs, ECOOP. Berlin Heidelberg: Springer-Verlag. 551–576.

Smith, G. (2000). The Object-Z Specification Language. Norwell: Kluwer Academic.

Spivey J.M. (1998). The Z Notation: A Reference Manual. United Kingdom: Prentice Hall International.

Spivey, J.M. (1988), Understanding Z: A Specification Language and its Formal Semantics. Cambridge: Cambridge University Press.

Warmer, J., & Kleppe, A. (1999). The Object Constraint Language: Precise Modeling with UML. Addison-Wesley.


  • There are currently no refbacks.

Copyright (c) 2015 Liudmyla Leonidivna Omelchuk

Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 International License.

ISSN (Print) : 2449-7320

ISSN (Online) : 2449-8726