Анализ линейно определенных итеративных циклов

Представлен новый метод доказательства инвариантности системы линейных неравенств, а также завершаемости линейно определенных итеративных циклов императивных программ. Тело цикла — линейный оператор, преобразующий вектор переменных программы. Метод учитывает предусловие цикла, а также условие повтор...

Ausführliche Beschreibung

Gespeichert in:
Bibliographische Detailangaben
Veröffentlicht in:Кибернетика и системный анализ
Datum:2016
1. Verfasser: Львов, M.C.
Format: Artikel
Sprache:Russian
Veröffentlicht: Інститут кібернетики ім. В.М. Глушкова НАН України 2016
Schlagworte:
Online Zugang:https://nasplib.isofts.kiev.ua/handle/123456789/131398
Tags: Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
Назва журналу:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Zitieren:Анализ линейно определенных итеративных циклов / M.C. Львов // Кибернетика и системный анализ. — 2016. — Т. 52, № 1. — С. 122-136. — Бібліогр.: 23 назв. — рос.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id nasplib_isofts_kiev_ua-123456789-131398
record_format dspace
spelling Львов, M.C.
2018-03-21T20:41:26Z
2018-03-21T20:41:26Z
2016
Анализ линейно определенных итеративных циклов / M.C. Львов // Кибернетика и системный анализ. — 2016. — Т. 52, № 1. — С. 122-136. — Бібліогр.: 23 назв. — рос.
0023-1274
https://nasplib.isofts.kiev.ua/handle/123456789/131398
004.421.6
Представлен новый метод доказательства инвариантности системы линейных неравенств, а также завершаемости линейно определенных итеративных циклов императивных программ. Тело цикла — линейный оператор, преобразующий вектор переменных программы. Метод учитывает предусловие цикла, а также условие повторения цикла в виде совокупности систем линейных неравенств. Метод основан на построении и анализе спектра этого оператора и вычислении числа итераций цикла, после выполнения которых инвариантность либо обеспечивается, либо опровергается. Теоретический материал работы иллюстрируется примерами.
Розглянуто новий метод доведення інваріантності системи лінійних нерівностей, а також завершуваності лінійно визначених ітеративних циклів імперативних програм. Тіло циклу — лінійний оператор, що перетворює вектор змінних програми. Метод враховує передумову циклу, а також умову повторення циклу у вигляді сукупності систем лінійних нерівностей. Метод ґрунтується на побудові та аналізі спектра цього лінійного оператора та обчисленні кількості ітерацій циклу, після виконання яких інваріантність або забезпечується, або спростовується. Теоретичний матеріал роботи проілюстровано прикладами.
The paper presents a new method to prove the invariance of the system of linear inequalities and termination 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 the 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 the linear operator and calculating the number of loop iterations after which the invariance is either provided or disproved. The theoretical material is illustrated by examples.
ru
Інститут кібернетики ім. В.М. Глушкова НАН України
Кибернетика и системный анализ
Программно-технические комплексы
Анализ линейно определенных итеративных циклов
Аналіз лінійно визначених ітеративних
Analysis of linear definite iterative loops
Article
published earlier
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
title Анализ линейно определенных итеративных циклов
spellingShingle Анализ линейно определенных итеративных циклов
Львов, M.C.
Программно-технические комплексы
title_short Анализ линейно определенных итеративных циклов
title_full Анализ линейно определенных итеративных циклов
title_fullStr Анализ линейно определенных итеративных циклов
title_full_unstemmed Анализ линейно определенных итеративных циклов
title_sort анализ линейно определенных итеративных циклов
author Львов, M.C.
author_facet Львов, M.C.
topic Программно-технические комплексы
topic_facet Программно-технические комплексы
publishDate 2016
language Russian
container_title Кибернетика и системный анализ
publisher Інститут кібернетики ім. В.М. Глушкова НАН України
format Article
title_alt Аналіз лінійно визначених ітеративних
Analysis of linear definite iterative loops
description Представлен новый метод доказательства инвариантности системы линейных неравенств, а также завершаемости линейно определенных итеративных циклов императивных программ. Тело цикла — линейный оператор, преобразующий вектор переменных программы. Метод учитывает предусловие цикла, а также условие повторения цикла в виде совокупности систем линейных неравенств. Метод основан на построении и анализе спектра этого оператора и вычислении числа итераций цикла, после выполнения которых инвариантность либо обеспечивается, либо опровергается. Теоретический материал работы иллюстрируется примерами. Розглянуто новий метод доведення інваріантності системи лінійних нерівностей, а також завершуваності лінійно визначених ітеративних циклів імперативних програм. Тіло циклу — лінійний оператор, що перетворює вектор змінних програми. Метод враховує передумову циклу, а також умову повторення циклу у вигляді сукупності систем лінійних нерівностей. Метод ґрунтується на побудові та аналізі спектра цього лінійного оператора та обчисленні кількості ітерацій циклу, після виконання яких інваріантність або забезпечується, або спростовується. Теоретичний матеріал роботи проілюстровано прикладами. The paper presents a new method to prove the invariance of the system of linear inequalities and termination 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 the 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 the linear operator and calculating the number of loop iterations after which the invariance is either provided or disproved. The theoretical material is illustrated by examples.
issn 0023-1274
url https://nasplib.isofts.kiev.ua/handle/123456789/131398
citation_txt Анализ линейно определенных итеративных циклов / M.C. Львов // Кибернетика и системный анализ. — 2016. — Т. 52, № 1. — С. 122-136. — Бібліогр.: 23 назв. — рос.
work_keys_str_mv AT lʹvovmc analizlineinoopredelennyhiterativnyhciklov
AT lʹvovmc analízlíníinoviznačenihíterativnih
AT lʹvovmc analysisoflineardefiniteiterativeloops
first_indexed 2025-12-07T19:26:38Z
last_indexed 2025-12-07T19:26:38Z
_version_ 1850878825522528256