Formal verification cycle programs
The article deals with an analytical approach to the assessment of the correctness of complex programs. On the example of the proof of the correctness of the program sorting is carried out check method of the program functions. Formalisms of the program functions allow a mathematically rigorous proof the correctness perform nested loops with arrays. Article results confirm the possibility of using this method in practice in software engineering.