Аннотация
В данной статье анализируется два способа анализа алгоритмов программного обеспечения. Первый из них основан на использовании механизма цепи рекурсии (chainrecurrences). Данный способ потенциально может существенно упростить задачу анализа в случае возможности представления программы в видебазовой рекурсии (baserecurrence), которая позволяет представить выражение под циклом в виде, из которого можно получить значение выражения на i-й итерации за O(1). Так как в настоящее время эта задача не решена, то метод анализа программ, основанный на цепях рекурсии, может быть применен только в ограниченном количестве программ (стоит сказать, что количество таких программ велико), где нет сложных циклов и выражений под ними.

Второй способ – это алгоритмический способ анализа. В статье приведена группа алгоритмов, с помощью которой можно выполнять проверку соотношений больше/меньше на произвольном массиве в программе. В качестве апробации был использован алгоритм сортировки вставкой. Приведенная группа алгоритмов проверки состоит из алгоритма определения путей в программе (при этом подразумевается, что пути строятся из расчета, что обратные ребра графа управления (controlflowgraph) входят в каждый путь только один раз), алгоритма анализа исследуемого соотношения в программе. Последний алгоритм предполагает предварительную обработку данных, которая не рассматривается в статье, но является достаточно простой, а также выполнение проверки соотношения на всей длине массива, без учета его составных частей. Алгоритм проверки может быть модифицирован (основная его часть будет сохранена) для проверки других видов соотношений.

Список литературы
1. Орлов С.А., Цилькер Б.Я. Технологии разработки программного обеспечения: современный курс по программной инженерии. – 4-е изд. – СПб.: Питер, 2012. – 608 с. – (Учебник для вузов) (Стандарт третьего поколения).

2. Верификация автоматных программ / С.Э. Вельдер, М.А. Лукин, А.А. Шалыто, Б.Р. Яминов; Санкт-Петербургский государственный университет информационных технологий, механики и оптики. – СПб.: Изд-во СПбГУ ИТМО, 2011. – 242 с.

3. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ. Model Checking. – М.: МЦНМО, 2002. – 416 с.

4. Карпов Ю.Г. Model checking. Верификация параллельных и распределенных программных систем. – СПб.: БХВ-Петербург, 2010. – 560 с.

5. Abramsky S., Hankin C. An introduction to abstract interpretation [Electronic resource]. – URL: https://www.cs.virginia.edu/~weimer/2007-615/reading/AbramskiAI.pdf (accessed: 10.03.2016).

6. Falk H., Marwedel P. Source code optimization techniques for data flow dominated embedded software. – New York: Springer Science: Business Media, 2004. – 226 p. – doi: 10.1007/978-1-4020-2829-8.

7. Cousot P., Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints // POPL'77: Proceedings of the 4^th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Los Angeles, California, 17–19 January 1977. – New York: ACM Press, 1977. – P. 238–252. – doi: 10.1145/512950.512973.

8. Coherent clusters in source code / S. Islam, J. Krinke, D. Binkley, M. Ha- rman // The Journal of Systems and Software. – 2014. – Vol. 88. – P. 1–24. – doi: 10.1016/j.jss.2013.07.040.

9. Horwitz S., Reps T., Binkley D. Interprocedural slicing using dependence graphs // ACM Transactions on Programming Languages and Systems. – 1990. – Vol. 12, iss. 1. – P. 26–60. – doi: 10.1145/77606.77608.

10. Ferrante J., Ottenstein K.J., Warren J.D. The program dependence graph and its use in optimization // ACM Transactions on Programming Languages and Systems. – 1987. – Vol. 9, iss. 3. – P. 319–349. – doi: 10.1145/24039.24041.

11. Handbook of automated reasoning / J.A. Robinson, A. Voronkov, eds. – Amsterdam: Elsevir Science; Cambridge: The Mit Press, 2001. – 2150 p.

12. Scholz B., Blieberger J., Fahringer T. Symbolic pointer analysis for detecting memory leaks // Proceedings of ACM SIGPLAN Workshop on "Partial Evaluation and Semantics-Based Program Manipulation" (PEPM’00), Boston, Massachusetts, USA, 22–23 January 2000. – New York: ACM Press, 2000. – P. 104–113. – doi: 10.1145/328690.328704.

13. Rugina R., Rinard M. Symbolic bounds analysis of pointers, array indices, and accessed memory regions // PLDI’00: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, Vancouver, Canada, 18–21 June 2000. – New York: ACM Press, 2000. – P. 182–195. – doi: 10.1145/358438.349325.

14. Bush W.R., Pincus J.D., Sielaff D.J. A static analyzer for finding dynamic programming errors // Software: Practice and Experience. – 2000. – Vol. 30, iss. 7. – P. 775–802. – 10.1002/(SICI)1097-024X(200006)30:7<775::AID- SPE309>3.0.CO;2-H.

15. Combining symbolic execution with model checking to verify parallel numerical programs / S.F. Siegel, A. Mironova, G.S. Avrunin, L.A. Clarke // ACM Transactions on Software Engineering and Methodology. – 2008. – Vol. 17, iss. 2. – P. 10:1–10:34. – doi: 10.1145/1348250.1348256.

16. Burgstaller B., Scholz B., Blieberger J. A symbolic analysis framework for static analysis of imperative programming languages // The Journal of Systems and Software. – 2014. – Vol. 85, iss. 6. – P. 1418–1439. – doi: 10.1016/j.jss.2011.11.1039.

17. Fahringer T., Scholz B. Advanced symbolic analysis for compilers. – Berlin; Heidelberg: Springer-Verlag, 2003. – 136 p. – (Lecture Notes in Computer Science; vol. 2628). – doi: 10.1007/3-540-36614-8.

18. Burgstaller B. Symbolic evaluation of imperative programming languages: technical report N 183/1-138 / Vienna University of Technology, Department of Avtomation. – Vienna, 2005. – 146 p.

19. Воевода А.А., Романников Д.О. Способы представления программ и их анализ // Сборник научных трудов НГТУ. – 2014. – № 3 (77). – C. 81–98.

20. Engelen R.A. van. The CR# algebra and its application in loop analysis and optimization: technical report TR-041223 / Florida State University. – Florida, 2004. – 13 p.