Introduction to the Atoment language

The Atoment language is a domain-specific language of development for program verification methods. It is used in the multilanguage software system Spectrum of rapid development and testing of verification methods. The easy-to-use specialized language allows a user of the system to describe verification methods in a natural notation, verify algorithms for different object domains adding new languages for their representations as necessary, share verification methods with other users and combine them. In this paper, an introduction to the Atoment language including a description of its main entities and examples of their use are given.