Анализ линейно определенных итеративных циклов / Львов M. C. (2016)
Ukrainian

інтернет-адреса сторінки: http://jnas.nbuv.gov.ua/article/UJRN-0000460187
  Кибернетика и системный анализ      А - 2019  /     Випуск (2016, Т. 52, № 1)

Львов M. C.
Анализ линейно определенных итеративных циклов

Розглянуто новий метод доведення інваріантності системи лінійних нерівностей, а також завершуваності лінійно визначених ітеративних циклів імперативних програм. Тіло циклу - лінійний оператор, що перетворює вектор змінних програми. Метод враховує передумову циклу, а також умову повторення циклу у вигляді сукупності систем лінійних нерівностей. Метод базується на побудові та аналізі спектра цього лінійного оператора та обчисленні кількості ітерацій циклу, після виконання яких інваріантність або забезпечується, або спростовується. Теоретичний матеріал роботи проілюстровано прикладами.

 https://doi.org/10.1007/s10559-016-9806-5
 Scopus

Бібліографічний опис:
Львов M. C.  Анализ линейно определенных итеративных циклов. Кибернетика и системный анализ. 2016. Т. 52, № 1. С. 122-136. doi: https://doi.org/10.1007/s10559-016-9806-5 URL: http://jnas.nbuv.gov.ua/article/UJRN-0000460187

English  Cybernetics and Systems Analysis   /     Issue (2016, 52 (1))

Lvov M.S.
Analysis of linear definite iterative loops

The paper presents a new method to prove the invariance of the system of linear inequalities and completability of linear definite iterative loops for imperative programs. Loop body is a linear operator that transforms the vector of program variables. The method takes into account loop precondition, as well as the condition of loop repetition in the form of a set of systems of linear inequalities. The method is based on the construction and analysis of the spectrum of linear operator and calculation of the number of loop iterations after which the invariance is either provided or disproved. The theory is illustrated by examples. © 2016, Springer Science+Business Media New York.

Keywords: invariant systems of linear inequalities, linear loop invariants, static program analysis, Invariance, Iterative methods, Mathematical operators, Imperative programs, Linear inequalities, Linear operators, Loop invariants, Loop iteration, Program variables, Static program analysis, System of linear inequalities, Mathematical transformations

Cite:
Lvov M.S. (2016). Analysis of linear definite iterative loops. Cybernetics and Systems Analysis, 52 (1), 122-136. doi: https://doi.org/10.1007/s10559-016-9806-5 http://jnas.nbuv.gov.ua/article/UJRN-0000460187 [In Russian].

 

Інститут інформаційних технологій НБУВ

+38 (044) 525-36-24
libnas@nbuv.gov.ua
Голосіївський просп., 3, к. 209
м. Київ, 03039, Україна