Статический анализ физических размерностей переменных программ и его реализация в алгебраическом программировании

Статический анализ физических размерностей переменных программ и его реализация в алгебраическом программировании

Збережено в:
Бібліографічні деталі
Дата:2017
Автор: Lvov, M.S.
Формат: Стаття
Мова:Ukrainian
Опубліковано: Інститут програмних систем НАН України 2017
Теми:
Онлайн доступ:https://pp.isofts.kiev.ua/index.php/ojs1/article/view/114
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Problems in programming
Завантажити файл: Pdf

Репозитарії

Problems in programming
id pp_isofts_kiev_ua-article-114
record_format ojs
resource_txt_mv ppisoftskievua/2e/a2b370620de7a0577af59a8770914e2e.pdf
spelling pp_isofts_kiev_ua-article-1142018-07-18T20:05:53Z Статический анализ физических размерностей переменных программ и его реализация в алгебраическом программировании Статичний аналіз фізичних розмірностей «перемінних» програм та його реалізація в алгебраїчному програмуванні Lvov, M.S. Физические программы Фізичні програми В работе рассматривается класс «физических» программ  т. е. программ, осуществляющих физические вычисления. Некоторые переменные таких программ имеют физический смысл, определяемый их физическими размерностями. Приведен алгоритм статического анализа исходного программного кода, проверяющий правильность использования переменных в соответствии с их физическими размерностями. Используются алгебраические модели программ, дополненные спецификациями физических размерностей входных и выходных переменных. Алгоритм интерпретирует эту модель, используя системы соотношений типа равенств из стандартной системы физических размерностей и семантику операторов алгебраической модели объектного языка программирования. Алгоритм реализован средствами алгебраического программирования системы APS-1. У роботі розглянуто клас «фізичних» програм програм, які здійснюють фізичні обчислення. Деяка частина змінних у таких програмах має фізичний смисл, який визначається їх фізичними розмірностями. Наведено алгоритм статичного аналізу програмного коду, перевіряючий правильність використання змінних у відповідності з їх фізичними розмірностями. Використана алгебраїчна модель вхідного програмного коду, доповнена специфікаціями фізичних розмірностей вхідних и вихідних змінних. Алгоритм інтерпретує цю модель, використовуючи таблиці співвідношень типа рівностей зі стандартної системи фізичних розмірностей і семантику операторів алгебраїчної моделі об’єктної мови програмування. Алгоритм реалізовано засобами алгебраїчного програмування системи APS-1. Інститут програмних систем НАН України 2017-06-14 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/114 PROBLEMS IN PROGRAMMING; No 2 (2015) ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2 (2015) ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2 (2015) 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/114/114 Copyright (c) 2017 ПРОБЛЕМИ ПРОГРАМУВАННЯ
institution Problems in programming
baseUrl_str https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date 2018-07-18T20:05:53Z
collection OJS
language Ukrainian
topic

spellingShingle

Lvov, M.S.
Статический анализ физических размерностей переменных программ и его реализация в алгебраическом программировании
topic_facet

Физические программы

Фізичні програми
format Article
author Lvov, M.S.
author_facet Lvov, M.S.
author_sort Lvov, M.S.
title Статический анализ физических размерностей переменных программ и его реализация в алгебраическом программировании
title_short Статический анализ физических размерностей переменных программ и его реализация в алгебраическом программировании
title_full Статический анализ физических размерностей переменных программ и его реализация в алгебраическом программировании
title_fullStr Статический анализ физических размерностей переменных программ и его реализация в алгебраическом программировании
title_full_unstemmed Статический анализ физических размерностей переменных программ и его реализация в алгебраическом программировании
title_sort статический анализ физических размерностей переменных программ и его реализация в алгебраическом программировании
title_alt Статичний аналіз фізичних розмірностей «перемінних» програм та його реалізація в алгебраїчному програмуванні
description
publisher Інститут програмних систем НАН України
publishDate 2017
url https://pp.isofts.kiev.ua/index.php/ojs1/article/view/114
work_keys_str_mv AT lvovms statičeskijanalizfizičeskihrazmernostejperemennyhprogrammiegorealizaciâvalgebraičeskomprogrammirovanii
AT lvovms statičnijanalízfízičnihrozmírnostejperemínnihprogramtajogorealízacíâvalgebraíčnomuprogramuvanní
first_indexed 2025-07-17T09:38:11Z
last_indexed 2025-07-17T09:38:11Z
_version_ 1838408937261498368
fulltext Теоретичні та методологічні основи програмування © М.С. Львов, 2015 ISSN 1727-4907. Проблеми програмування. 2015. № 2 3 УДК 004.421.6 М.С. Львов СТАТИЧЕСКИЙ АНАЛИЗ ФИЗИЧЕСКИХ РАЗМЕРНОСТЕЙ ПЕРЕМЕННЫХ ПРОГРАММ И ЕГО РЕАЛИЗАЦИЯ В АЛГЕБРАИЧЕСКОМ ПРОГРАММИРОВАНИИ В работе рассматривается класс «физических» программ  т. е. программ, осуществляющих физиче- ские вычисления. Некоторые переменные таких программ имеют физический смысл, определяемый их физическими размерностями. Приведен алгоритм статического анализа исходного программного кода, проверяющий правильность использования переменных в соответствии с их физическими размерно- стями. Используются алгебраические модели программ, дополненные спецификациями физических размерностей входных и выходных переменных. Алгоритм интерпретирует эту модель, используя си- стемы соотношений типа равенств из стандартной системы физических размерностей и семантику опе- раторов алгебраической модели объектного языка программирования. Алгоритм реализован средства- ми алгебраического программирования системы APS-1. Введение Компьютерные программы, в кото- рых реализованы физические вычисления, должны удовлетворять нескольким спе- цифическим свойствам. Одно из таких свойств заключается в корректном ис- пользовании размерных физических вели- чин. Вычисления в «физических» про- граммах основаны на формулах физиче- ских законов, переменные которых, кроме имени, типа и значения, имеют еще одну характеристику – физическую размер- ность. Современные языки программиро- вания не используют по умолчанию ни ти- пизации переменных по их физическому смыслу, ни, тем более, физических раз- мерностей констант и переменных. Даже языки со строгой типизацией, поддержи- вающие перегрузку арифметических опе- раций, не вполне пригодны для определе- ния специальных физических типов дан- ных. В самом деле, эти типы определяются векторами физических размерностей, по- этому вычисление типа значения арифме- тического выражения требует вычислений в векторном пространстве, определенном одной из стандартных систем физических размерностей (например, Си, таблица). Поэтому ошибки в программах, связанные с неправильным использованием физиче- ских размерностей, не выявляются ни во время компиляции, ни во время исполне- ния программы. Таким образом, возникает задача разработки программы, проверяющей пра- вильность использования переменных по их физическим размерностям. Пользова- тель должен специфицировать все входные и выходные переменные программы их физическими размерностями, а программа должна проверить правильность этой спе- цификации. Алгоритм анализа программного кода опирается на соотношения типа ра- венств – физические законы и правила си- стем физических размерностей, которые естественно представят в виде систем пе- реписывающих правил. Например, соот- ношение Вольт=Ампер*Ом – закон Ома в системе Си. Это означает, что если в про- грамме есть оператор присваивания I:=A*R, то переменная I должна иметь такую же физическую размерность, как и выражение *A R . Практика показывает, что многие алгоритмы анализа программ могут быть эффективно реализованы средствами ал- гебраического программирования, т. е. в виде совокупности систем переписываю- щих правил. Такие алгоритмы описыва- ются особенно просто, если использовать алгебраические модели объектных про- грамм. Таким образом, объект исследова- ния – приложения методологии алгебраи- ческого программирования к задачам ста- тического анализа программ, а предмет Теоретичні та методологічні основи програмування 4 исследования – разработка алгебраиче- ской программы анализа правильности использования «физических» переменных в программах. 1. Постановка проблемы Пусть ( )PP W – математическая мо- дель программы и PW – множество ее пе- ременных. Физической размерностью пе- ременной Px W назовем элемент n r Rat векторного пространства n Rat над полем рациональных чисел, а физической вели- чиной (интерпретированной переменной) – пару ,x r . Физической интерпретацией ( )PInt W программы ( )PP W назовем мно- жество физических величин: ( ) { , : }P PInt W x r x W   . Требуется по- строить алгоритмическую функцию * * P( , ), если Int(W ) ( , ) определена корректно; впротивном случае. P Int PhInt P Int         Функция ),( IntPPhInt должна быть опи- сана средствами алгебраического про- граммирования, т. е. в виде систем пере- писывающих правил. Предполагается, что исходный программный код про- граммы P синтаксически правилен и его математическая модель построена пра- вильно. Задача построения математичес- кой модели исходной программы здесь не рассматривается. Математическая модель класса ис- следуемых программ описана в разделе 3. Функция ( , )PhInt P Int , определяющая и проверяющая корректность интерпрети- рованной программы, описана в разделе 4. Отметим, что заключительная программа *P – программа без циклов такая, что * * * ( , ) ( , )PhInt P Int P Int . Заключительная интерпретация * Int содержит вычислен- ные физические размерности локальных переменных. 2. Обзор литературы Как показано в [1], рассматриваемая задача решается методами статического анализа программного кода. Причины, по которым необходим статический анализ для верификации программ этого типа – так называемого программного обеспече- ния критического оборудования обсуж- даются в [2–4]. Еще один класс такого программного обеспечения – программы учебного назначения. Таким образом, за- дача актуальна. Технологии алгебраического про- граммирования [5, 6] успешно исполь- зуются для разработки программного обеспечения во многих предметных обла- стях [7–9], в том числе и в задачах ста- тического анализа программ [10]. Практи- ка показала, что в качестве модели объ- ектной программы удобно использовать выражения в алгебре алгоритмов Глуш- кова [11]. В настоящей статье описано по- строение алгебраической функции, эф- фективно решающей задачу статического анализа правильности применения «физи- ческих» переменных в программах. В ка- честве модели объектной программы ис- пользуется выражение в алгебре алгорит- мов Глушкова. Тем самым показано, что в терминах алгебраического программиро- вания алгоритм по существу представляет собой спецификации объектной програм- мы в виде систем переписывающих правил и одновременно эффективную программу статического анализа программного кода, работающую «на лету». 3. Модель программы 3.1. Модель памяти программы. Пусть 1 2( , ,..., )kX x x x – вектор входных переменных программы P ; 1 2( , ,..., )mY y y y – вектор выход- ных переменных программы P ; 1 2( , ,..., )lZ z z z – вектор локаль- ных переменных программы P . Памятью программы назовем мно- жество W X Y Z   . Физической размерностью перемен- ной x W назовем вектор 1( ,..., )nr r r n -мерного векторного пространства n Rat , где Rat – поле рациональных чисел. Теоретичні та методологічні основи програмування 5 Таблица. Основные и производные единицы системы Си Название и обозначение величины Единица измерения Обозначение Формула Показатели степени м кг с А К кд Длина L Метр M L 1 Масса M Килограмм Kg M 1 Время T Секунда S T 1 Сила электр. тока I Ампер A I 1 Термодинамическая температура T Кельвин K T 1 Сила света Iv Кандела Cd J 1 Сила F Ньютон N F = ma 1 1 −2 Давление P Паскаль Pa P = F/S −1 1 −2 Работа, энергия A Джоуль J A = F·L 2 1 −2 Импульс P kg·m/s p = m·v 1 1 −1 Мощность P Ватт W P = A/t 2 1 −3 Электрический заряд Q Кулон C q = I·t 1 1 Электрическое напряжение, электрический потенциал U Вольт V U = A/q 2 1 −3 −1 Физической величиной u назовем пару , , , n u x r x W r Rat    . Если u – физическая величина, то, по определению, x – ее идентификатор, а r – физическая размерность. Определение размерности физичес- кой величины связывает единицу измере- ния (идентификатор размерности) с векто- ром показателей степеней основных физи- ческих величин системы физических раз- мерностей, выбранной в качестве стан- дартной. Фрагмент такого определения представлен в таблице. Отметим, что на практике можно расширить язык специфи- каций таблицей имен единиц измерения физических величин. Например, вместо спецификации , (2,1, 3,0,0,0)W   можно использовать ,W Ватт  . 3.2. Модель вычислений. Опера- тор присваивания имеет вид 1 2: ( , , , ),jv f u u u  1 2, ,..., ,ju u u v W . (1) Алгебраические выражения в пра- вых частях операторов присваивания определены в сигнатуре термов (операций) () (), () (), ()*(), () / (), () ^ , (), ().nn  (2) Физическая размерность выраже- ния правой части оператора присваивания определяется следующими правилами: <x,r> + <y,r> = <x + y, r>, (3) <x,r> - <y,r> = <x - y, r>, C*<x,r> = <C*x, r>,// Умножение на безраз- мерную константу <x, r1>*<y, r2> = <x*y, r1 + r2>, <x,r1>/<y,r2> = <x*y, r1 - r2>, <x,r>^n = <x^n, n*r>, Sqrt(<x, r>) = <Sqrt(x), r/2>, Sqrtn(<x, r>) = <Sqrtn(x), r/n>. Отметим, что аддитивные операции над физическими величинами определены частично – только в случае, когда физиче- ские размерности обеих операндов совпа- дают. Иначе в выражении допущена ошибка, сигнализируемая специальным Теоретичні та методологічні основи програмування 6 символом  (wrong), которая выявляется правилами r1<>r2  <x,r1> + <y,r2> = , (3) r1<>r2  <x,r1> - <y,r2> = . Физической интерпретацией опера- тора присваивания (1) называется пара 1( , , ( ,..., ), )v n fv r f u u r    , вычисленная по правилам (3, 3). Физической интерпре- тацией оператора присваивания (1) назы- вается корректной, если vr определена и v fr r . В противном случае возможны три варианта: v1. vr не определена (переменная v не интерпретирована). v2. Переменная v интерпретирована повторно. v3. В программе допущена ошибка ин- терпретации. Условия в операторах управления программы – суть бескванторные формулы прикладной логики предикатов в сигнату- ре термов (2), сигнатуре атомарных преди- катов-условий () (), () (), () ()   и сиг- натуре логических связок ().(),()(),&()  Физические размерности атомар- ных условий определяются правилами <x,r> > <y,r> = x > y, <x,r> = <y,r> = x = y, <x,r>  <y,r> = x  y, (4) r1<> r2  <x,r1> > <y,r2> = , r1<> r2  <x,r1> = <y,r2> = , r1<> r2  <x,r1>  <y,r2> = . Таким образом, сравнимы физичес- кие выражения одинаковой физической размерности. В противном случае в срав- нении допущена ошибка, сигнализируемая символом  . Поэтому физическая интер- претация атомарного условия называется корректной, если она не равна  . Физиче- ская интерпретация составного условия называется корректной, если корректны все физические интерпретации ее атомар- ных условий. Замечание. В настоящей версии алгоритма анализа использование различ- ных, но сравнимых размерностей приво- дит к генерации признака ошибки. Так, размерности секунда и минута считаются различными, и алгоритм анализа сгенери- рует значение . Таким образом, если в формуле используются две величины сравнимых размерностей, пользователь сам должен решить, допущена ошибка или различие в этих размерностях учте- но домножением на соответствующую константу. 3.3. Модель управления. Операто- ры управления программы – условные операторы и операторы циклов If U then P, If U then P else Q, While U do P, Repeat P until U. с общепринятой семантикой. Таким обра- зом, мы ограничиваемся структурирован- ными программами (процедурами, функ- циями). В соответствии с определениями выражения в алгебре алгоритмов Глушко- ва в дальнейшем используется следующая алгебраическая и функциональная формы записи операторов управления: P; Q // Последовательное выполнение If U then P ~ U P I , If(U,P) If U then P else Q ~ U P Q , Ifelse(U,P,Q) While U do P ~ { } U P , While(U,P) Repeat P until U. ~ { } U P .Repeat(U,P) Множество всех операторов при- сваивания в программе P обозначим ( )Ass P , а множество всех условий – ( )Cond P . 3.4. Физическая интерпретация программы определяется множеством фи- зических величин , , , R R R R W X Y Z  1 11 1, ,..., . R k kX x r x r    , 1 21 2, ,..., . R m mY y r y r    , 1 31 3, ,..., . R l lZ z r z r    . Исходной физической специфика- цией называется множество Теоретичні та методологічні основи програмування 7 0 , R R R W X Y  . Это множество задается пользова- телем. Будем считать, что исходные физи- ческие интерпретации не могут изменяться в процессе вычислений. Если одна из пе- ременных множества X Y интерпрети- руется повторно в результате выполнения оператора присваивания, ее новая интер- претация должна совпадать с исходной. Иначе в программе допущена ошибка  физической интерпретации. Заметим, что в языках програм- мирования повторная интерпретация лю- бых переменных допустима, если выпол- нен контроль типов. Вектор Z локальных переменных не специфицирован. Таким образом, для исходной интерпретации переменных из Z алгоритм использует специальный сим- вол  . Исходная интерпретация перемен- ной z Z имеет вид ,z   . { , | }.Z z z Z      Исходной физической интерпрета- цией программы P называется множество , , R R R W X Y Z     . Обозначим это мно- жество (0) Int . Для вычисления физической интерпретации программы P с исходной интерпретацией (0) Int введем специаль- ную функцию ( , )PhInt P Int , отображаю- щую программу P с исходной интерпре- тацией (0) Int в ее заключительную физи- ческую интерпретацию: : R R PhInt P W P W   . Если )(WP – программа над памятью ZYXW  , не содержащая ни одного оператора, ( , ) ( , ). R R oPhInt P W P W Пусть P – программа, представлен- ная в алгебраической форме. Путем w в программе P назовем последовательность операторов присваивания и условий 1 2... Ns s s , выполняемых последовательно при исполнении программы: 1 2... , ( ) ( )N jw s s s s Ass P Cond P   . Точное определение пути – это ин- дуктивное определение по структуре формулы программы. Оно будет сформу- лировано при доказательстве основной теоремы. Программу P будем ассоциировать с множеством ее путей точно так же, как регулярное выражение ассоциируется с регулярным языком – множеством слов, определенных этим выражением. Поэтому имеет смысл отношение w P . Пусть (0) Int – исходная физическая интерпретация. Выполнение программы P вдоль пути w преобразует интер- претацию (0) Int в интерпретацию ( )w Int . Физическая интерпретация пути w в программе P называется корректной, если ( )w Int  . Физическая интерпрета- ция программы P называется коррект- ной, если все интерпретации ( ) , w Int w P корректны. Правила вычисления интерпрета- ции пути заданы функциями PhIntExpr , PhIntCond , PhIntAss и правилами интер- претации последовательного выполнения, сформулированными ниже. 4. Алгоритм и алгебраическая программа анализа физических размерностей 4.1. Основные функции алгебраи- ческой программы. На предварительном этапе алгоритм заменяет в специфицира- ванной программе P все переменные сво- ими исходными физическими интерпрета- циями из Int , используя систему перепи- сывающих правил, определенную табли- цей размерностей физических величин стандартной системы физических размер- ностей (см. таблицу). Вычисления физических интерпре- таций арифметических выражений и условий осуществляют функции ( , )Ph Int Expr f Int , ( , )Ph Int Cond U Int , осно- ванные на системах переписывающих пра- вил, расширяющих соответственно (3), (4). Замена переменной ее физической величиной реализована подстановкой в структуры данных арифметических вы- ражений и условий вместо переменных указателей на соответствующие физиче- Теоретичні та методологічні основи програмування 8 ские величины в списке физических вели- чин R W . Таким образом,  rx, реализо- вана как указатель на структуру (x, r) – элемент списка. Такая реализация поз- воляет изменять вектор r одновременно во всех вхождениях переменой x в про- грамму. Системы переписывающих пра- вил интерпретирующих функций на внешнем языке Aplan системы програм- мирования APS имеют вид: PhIntExpr := rs(x,y,r,r1,r2 C){ IsConst(C) C = <Const, 0>, <x,> = return(), <x,r> + <y,r> = <x + y, r>, r1<>r2  <x,r1>+<y,r2> = return(), <x,r> - <y,r> = <x – y, r>, r1<>r2  <x,r1>-<y,r2> = return(), <x, r1>*<y, r2> = <x*y, r1+r2>, <x,r1>/<y,r2> = <x*y, r1 – r2>, <x,r>^n = <x^n, n*r>, Sqrt(<x, r>) = <Sqrt(x), r/2>, Sqrtn(<x, r>) = <Sqrtn(x), r/n> }; PhIntCond := rs(x,y,r1,r2,L,R){ L > R = PhIntExpr(L)> PhIntExpr(R), L = R = PhIntExpr(L)= PhIntExpr(R), L  R = PhIntExpr(L) PhIntExpr(R), r1<>r2 <x,r1> > <y,r2> = return(), r1<>r2 <x,r1> = <y,r2> = return(), r1<>r2 <x,r1>  <y,r2> = return() }; Правила вычисления физической интерпретации оператора присваивания имеют вид: PhIntAss := rs(u, f, r, r1, r2){ //вариант v1 <u, > := <f, r> = <u, r>, // вариант v2 uZ)<u, r1> := <f, r2>=<u, r2>, // вариант v3 (uXY)&(r1<>r2)<u,r1> := <f, r2> = return() }; Определим теперь физические ин- терпретации для каждого оператора управления. // RO. Прерывание и обработка ис- ключительной ситуации PhInt(P, ) = return(); // R1. Интерпретация оператора присваивания PhInt(u:=v, Int)=PhIntAss(u:=v, Int); // R2. Интерпретация последова- тельного выполнения PhInt(P;Q, Int) = PhInt(Q, PhInt(P,Int)); // R3. Интерпретация неполного ветвления. Интерпретации ветвей должны быть равны PhIntCond(U, Int)=   PhInt(If(U,P), Int) = return(), PhInt(P, Int)<> Int  PhInt(If(U,P), Int) = return(), PhInt(If(U,P), Int) = Int; // R4. Интерпретация полного ветв- ления. Интерпретации ветвей должны быть равны PhIntCond(U)==   PhInt(Ifelse(U,P,Q),Int) = return(), (PhInt(P)<> PhInt(Q)) PhInt(Ifelse(U,P,Q),Int) = return(), PhInt(Ifelse(U,P,Q),Int) = PhInt(P, Int); // R5. Интерпретация цикла While PhIntCond(U)=   PhInt(While(U,P), Int) = return(), PhInt(P, Int)<> Int  PhInt(While(U,P), Int) = return(), PhInt(While(U,P), Int) = PhInt(P); // R6. Интерпретация цикла Repeat. Выполнение P изменяет интерпретацию U . PhInt(P, Int))=   PhInt(Repeat(U,P), Int) = return(), PhIntCond(U,PhInt(P,Int))=PhInt(Re peat(U,P),Int) = return(), PhInt(P,Int)<>PhInt(P,PhInt(P,Int)) PhInt(Repeat(U,P),Int)= return(), PhInt(Repeat(U,P), Int) = PhInt(P); Теоретичні та методологічні основи програмування 9 Физическая интерпретация Int про- граммы P равна (0) ( , )PhInt P Int . Отме- тим, что для функции PhInt выполняются следующие основные свойства: 1) только два правила системы PhIntAss изменяют интерпретацию, не прерывая работы алгоритма ввиду ошиб- ки интерпретации – это правила вариан- тов 1 и 2; 2) правила интерпретации условий PhIntCond не изменяют корректных ин- терпретаций; 3) правила интерпретации операто- ров управления R3–R6 требуют, чтобы интерпретации вдоль различных путей вычислений, определяемых этими опера- торами, совпадали. Поскольку интер- претации переменных из множества YX  зафиксированы в спецификациях, это относится к переменным из Z . Точ- нее, если 11 12 1 1 21 22 2 2, ,..., , , ,...,j js s s s s s – два пути в одном операторе управления, вычисления вдоль каждого из путей могут менять интерпретации локальных пере- менных, но результирующие интерпрета- ции должны совпасть. 4.2. Основная теорема. Теорема. Алгоритм, определенный правилами PhIntExpr , PhIntCond , PhIntAss , R0–R6 правильно вычисляет физическую интер- претацию программы P . Доказательство. Мы покажем, что (0) ( , )PhInt P Int  тогда и только тогда, когда в программе P существует путь w такой, что ( )w Int  . Доказательство бу- дем вести индукцией по структуре форму- лы программы. 1. Предположим, что (0) ( , )PhInt P Int  . Анализ правил алгоритма PhInt показы- вает, что ошибка, если она обнаруживает- ся алгоритмом, генерируется вдоль путей, получаемых выполнением операторов в каждом цикле некоторое минимально не- обходимое количество раз. Назовем такие пути простыми. Точное определение про- стых путей будет задано формулами в ин- дуктивных шагах доказательства. а) (базис индукции) , ( ) { }.P s Ass P s  Путь sw  является простым. б) 1 2;P Q Q . По правилу R2 PhInt(Q1;Q2,Int(0)) = PhInt(Q2, PhInt(Q1,Int(0))) = . Тогда либо PhInt(Q1,Int(0)) =  и по правилу R0 PhInt(Q2, ) = , либо PhInt(Q1,Int(0)))   и PhInt(Q2, PhInt(Q1,Int(0))) = . Если PhInt(Q1,Int(0)) = , по предположению индукции существует простой путь 1 1w Q такой, что 1( )w Int  . Тогда для любого простого пу- ти 2 2w Q искомым является простой путь 1 2w w . Если PhInt(Q1,Int(0))), по предположению индукции, все интерпре- тации 1( ) 1 1, w Int w Q корректны. Следо- вательно, корректны интерпретации вдоль простых путей из 1Q . Любой путь из P начинается с некоторого пути 1w из 1Q . Выберем все простые пути из 2Q . По предположению индукции, ошибка должна быть обнаружена вдоль некоторого про- стого пути 2w . Тогда ошибка интерпрета- ции в P обнаруживается вдоль простого пути 1 2w w w . Простые пути задаются формулой 1 2;P Q Q ; в) U P Q I  . По правилу R3, ошибка обнаруживается либо в интерпре- тации условия, либо в интерпретации программы Q . Если интерпретация усло- вия корректна, по предположению индук- ции ошибка обнаруживается вдоль про- стого пути из Q . В противном случае программа Q может не выполняться ни одного раза. Поскольку правила интер- претации условий не меняют корректных Теоретичні та методологічні основи програмування 10 интерпретаций, простые пути задаются формулой P U Q  ; г) 1 2 U P Q Q  . По правилу R4, ошибка обнаруживается либо в интерпре- тации условия, либо в интерпретации про- грамм 1 2,Q Q . Если интерпретация усло- вия корректна, по предположению индук- ции ошибка обнаруживается либо вдоль простого пути из 1Q , либо вдоль простого пути из 2Q . В противном случае програм- мы 1 2,Q Q могут не выполняться ни одно- го раза. Отметим, что после выполнения 1 2 U P Q Q  интерпретации вдоль различ- ных путей должны совпадать. Иначе обна- руживается ошибка интерпретации. Про- стые пути задаются формулой 1 2;P U Q Q  ; д) }{QP U  . По правилу R5, ошибка обнаруживается либо в интер- претации условия U , либо в интерпрета- ции программы Q . Если интерпретация условия корректна, по предположению индукции ошибка обнаруживается вдоль простого пути из Q . В противном случае программа Q может не выполняться ни одного раза. Следовательно, при выпол- нении Q интерпретация не должна ме- няться. Простые пути задаются формулой P U Q  ; е) { } U P Q . По правилу R6, ошибка обнаруживается либо в теле цикла Q , либо в интерпретации условия U по- сле однократного выполнения тела цикла. Если ошибка не обнаружена, интерпрета- ция программы P равна интерпретации тела цикла Q при исходной интерпре- тации. Повторное выполнение тела цик- ла Q не должно изменить интерпре- тации. По предположению индукции, ошибка обнаруживается вдоль простого пути из Q . Простые пути задаются фор- мулой ; ;P Q U Q Q  . 2. Предположим, что в про- грамме P существует путь w такой, что ( )w Int  . а) (базис индукции) , ( ) { }.P s Ass P s  В этом случае sw  . И ( )w Int , и (0) ( , )PhInt P Int вычисляется одними и теми же правилами PhIntAss (правило R1). Следовательно, ( )w Int = (0) ( , )PhInt P Int =  . Заметим, что в этом случае имеет место вариант v3 правил, т. е. интерпретации левой и правой частей оператора s раз- личны; б) 1 2;P Q Q (см. п. б)) предыду- щего доказательства; в) U P Q I  . Тогда ;P U Q U  . Поскольку U не меняет интерпретации, U также не меняет интерпретации. Наконец, интерпретации QU ; и U должны совпасть. Следовательно, ошибка должна быть обнаружена вдоль путей QU  ; г) 1 2 U P Q Q  . Рассуждения, ана- логичные предыдущим, приводят к путям 1 2;U Q Q ; д) { } U P Q . Рассуждения, анало- гичные п. в), приводят к путям U Q ; е) { } U P Q , ; ; ; ; ; ; ; ; ; ...P Q U Q U Q U Q U Q U U Q      Поскольку интерпретации ; , ; ; ;Q U Q U Q U , если они корректны, должны совпадать, то и интерпретации QQQ ;, должны сов- падать. Если эти интерпретации совпада- ют, повторное вычисление тела Q вдоль пути ;Q Q не изменяет интерпретации P . Следовательно, и последующие вычисле- ния ; ; ...Q Q Q уже не изменят интерпрета- ции P . Теорема доказана. Теоретичні та методологічні основи програмування 11 5. Дискуссия Основное свойство, на котором по- строено доказательство основной теоремы – свойство 3. Можно привести пример, в котором это свойство нарушено, а про- грамма все-таки имеет корректную физи- ческую интерпретацию. Однако, с нашей точки зрения, это плохой стиль програм- мирования, когда, например, в одной ветви вычислений переменная T обозначает вре- мя, а в другой – той же переменной T обо- значена температура. Алгоритм анализа ориентирован на применение к процедурам и функциям. Однако нет никаких проблем распростра- нения его на модули и программные си- стемы. Модель программы использует только простые переменные. Однако пла- нируется распространить его и на состав- ные типы данных, что требует усложне- ния модели памяти и анализа раздела ти- пов. Заключение Значение функции (0) ( , )PhInt P Int вычисляется стандартной стратегией «снизу-вверх». Значения аргументов при этом не перевычисляются. Поэтому ин- терпретатор, описанный в работе, по спецификациям исходной программы строит программу без циклов *P за один проход. Поэтому алгебраическая про- грамма PhInt эффективна – она проверя- ет правильность использования физиче- ских размерностей «на лету». Заметим, что алгоритм, приведенный в [1], строит и решает систему линейных уравнений, что не эффективно. Проблема построения алгебраичес- кой модели объектной программы здесь не рассматривается. Однако, поскольку про- граммы на языках процедурного програм- мирования по существу представляют со- бой алгебраические объекты, эта проблема средствами алгебраического программи- рования может быть решена эффективно. Как показано в [2–4], задача анализа физи- ческих размерностей – одна из основных задач разработки программного обеспече- ния критического оборудования. Поэтому ее дальнейшее развитие имеет большое практическое значение. Автор благодарит профессора Г.Н. Жолткевича за формулировку про- блемы и полезные ее обсуждения, а также академика А.А. Летичевского за многолет- нее сотрудничество в области алгебраиче- ского программирования. 1. Briukhankov S.S., Konoriev B.M., Lvov M.S., Zholtkevitch H.N. About the Static Variable Dimensions Analysis for Software of Critical Appliance (English) // Radioelectronic and Computing Systems. N 6(47). Kharkiv “KHAI”. – 2010. – P. 186–191. 2. Rushby J.M. Formal Verification of Algo- rithms for Critical Systems // IEEE Trans. Soft. Eng. – 1993. – Vol. 19, N 1. – P. 13–23. 3. Binkley D. Source Code Analysis: A Road Map // Future of Software Engineering 2007. – IEEE: Proc. FOSE’07, 2007. – P. 89–105. 4. Konorev B.M., Kharchenko V.S,. Chertkov G.N., Alekseev Yu.G., Manzhos Yu.S., Ser- gienko V.V. Integrated Instrumental Environ- ment for Critical-Mission Software Systems Assessment, in Russian // Kharkiv: I&C Sys- tem Certification Centre. State Centre for Regulation of Supplies and Service of Quality of State Nuclear Regulatory Committee of Ukraine, 2005. – 258 p. 5. Letichevsky А.А., Kapitonova J., Volkov V. and others. Algebraic Programming System APS: User Manual // Glushkov Institute of Cybernetics, National Acad. of Sciences of Ukraine, Kiev, Ukraine, 1998. – 50 p. 6. Kapitonova J., Letichevsky A., Lvov M., Volkov V. Tools for Solving Problems in the Scope of Algebraic Programming // Lecture Notes in Computer Sciences. – N 958. – 1995. – Р. 31–46. 7. Lvov M.S. Algebraic approach to the problem of solving systems of linear inequalities // Cy- bernetics and Systems Analysis. – 2010. – Vol. 46, N 2. – Р. 326–338. 8. Lvov M.S., Peschanenko V.S. Trapezoid method for solving systems of linear inequali- ties and its implementation in insertion mod- eling // Cybernetics and Systems Analysis. – 2012. – Vol. 48, N 4. – Р. 931–942. 9. Letichevsky A., Letychevskyi O., Peschanenko V. About One Efficient Algorithm for Reach- ability Checking in Modeling and Its Imple- mentation // Communications in Computer http://link.springer.com/article/10.1007/s10559-010-9210-5 http://link.springer.com/article/10.1007/s10559-010-9210-5 http://www.springerlink.com/content/106467/?p=d9e06ef0201947e6a7576d36fd74315c&pi=0 http://www.springerlink.com/content/106467/?p=d9e06ef0201947e6a7576d36fd74315c&pi=0 http://www.springerlink.com/content/j2561rg6t0v8/?p=d9e06ef0201947e6a7576d36fd74315c&pi=0 http://www.springerlink.com/content/106467/?p=d9e06ef0201947e6a7576d36fd74315c&pi=0 http://www.springerlink.com/content/j2561rg6t0v8/?p=d9e06ef0201947e6a7576d36fd74315c&pi=0 https://docs.google.com/viewer?a=v&pid=sites&srcid=ZGVmYXVsdGRvbWFpbnx2bGFkaW1pcnBlc2NoYW5lbmtvfGd4OjdiMTZhMDU3MzkyOWU2YTc https://docs.google.com/viewer?a=v&pid=sites&srcid=ZGVmYXVsdGRvbWFpbnx2bGFkaW1pcnBlc2NoYW5lbmtvfGd4OjdiMTZhMDU3MzkyOWU2YTc https://docs.google.com/viewer?a=v&pid=sites&srcid=ZGVmYXVsdGRvbWFpbnx2bGFkaW1pcnBlc2NoYW5lbmtvfGd4OjdiMTZhMDU3MzkyOWU2YTc Теоретичні та методологічні основи програмування 12 and Information Science. – 2012. – N 149. – P. 149–165. 10. Lvov M.S. Polynomial invariants for linear loops. // Сybernetics and Systems Analysis. – 2010. – Vol. 46, Issue 4. – P. 660–668. 11. Глушков В.М., Цейтлин Г.Е., Ющенко Е.Л. Алгебра. Языки. Программирование. 3-е изд., перераб. и доп. – Киев: Наук. думка, 1989. – 376 с. Получено 21.11.2014 Об авторе: Львов Михаил Сергеевич, доктор физико-математических наук, доцент, профессор кафедры информатики, программной инженерии и экономической кибернетики. Место работы автора: Херсонский государственный университет, ул. 40-летия Октября, 27. 73000 Херсон, Украина. Тел: +380552 32 67 81, +380552 43 23 15. E-mail: lvov@ksu.ks.ua https://docs.google.com/viewer?a=v&pid=sites&srcid=ZGVmYXVsdGRvbWFpbnx2bGFkaW1pcnBlc2NoYW5lbmtvfGd4OjdiMTZhMDU3MzkyOWU2YTc https://docs.google.com/viewer?a=v&pid=sites&srcid=ZGVmYXVsdGRvbWFpbnx2bGFkaW1pcnBlc2NoYW5lbmtvfGd4OjdiMTZhMDU3MzkyOWU2YTc http://www.springerlink.com/content/?Author=M.+S.+Lvov http://www.springerlink.com/content/kv81383w6162884t/ http://www.springerlink.com/content/kv81383w6162884t/

Схожі ресурси