СБОРНИК
НАУЧНЫХ ТРУДОВ НГТУ

ISSN: 2307-6879
English | Русский

Последний выпуск
№2(92) Апрель - Июнь 2018

Алгоритм анализа массива в программе с использованием произвольных проверок

Выпуск № 4 (82) Октябрь - Декабрь 2015
Авторы:

А.А. ВОЕВОДА,
Д.О. РОМАННИКОВ
DOI: http://dx.doi.org/10.17212/2307-6879-2015-4-92-107
Аннотация
В данной статье анализируется два способа анализа алгоритмов программного обеспечения. Первый из них основан на использовании механизма цепи рекурсии (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 4th 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.

 
Просмотров: 403