Backward transformation of formulas in symbolic modeling: from the result to the source formula
Logical formulas over attributes set are analog of system states in symbolic modeling of transition systems. Transition rules of source system are the base for building of modeling rules which operate on formula state and define transition from source state to the next or previous state. Predicate t...
Gespeichert in:
| Datum: | 2026 |
|---|---|
| Hauptverfasser: | , |
| Format: | Artikel |
| Sprache: | Russisch |
| Veröffentlicht: |
PROBLEMS IN PROGRAMMING
2026
|
| Schlagworte: | |
| Online Zugang: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/923 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Institution
Problems in programming| _version_ | 1866844947762642944 |
|---|---|
| author | Godlevsky, A.B. Potienko, S.V. |
| author_facet | Godlevsky, A.B. Potienko, S.V. |
| author_institution_txt_mv | [
{
"author": "A.B. Godlevsky",
"institution": "Glushkov Institute of Cybernetics NAS of Ukraine"
},
{
"author": "S.V. Potienko",
"institution": "Glushkov Institute of Cybernetics NAS of Ukraine"
}
] |
| author_sort | Godlevsky, A.B. |
| baseUrl_str | https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| collection | OJS |
| datestamp_date | 2026-06-01T06:02:58Z |
| description | Logical formulas over attributes set are analog of system states in symbolic modeling of transition systems. Transition rules of source system are the base for building of modeling rules which operate on formula state and define transition from source state to the next or previous state. Predicate transformer is an algorithm which models transitions in the formula state space. We describe backward predicate transformer which has distinguishing feature that modeled transitions allow as assignment operators over simple and complex data structures (arrays and lists) as constraints which define attribute changes implicitly.Problems in programming 2010; 2-3:363-368 |
| first_indexed | 2026-06-02T01:01:19Z |
| format | Article |
| fulltext |
Формальні методи програмування
© А.Б. Годлевский, С.В. Потиенко, 2010
ISSN 1727-4907. Проблеми програмування. 2010. № 2–3. Спеціальний випуск 363
УДК 519.686.2
ОБРАТНАЯ ТРАНСФОРМАЦИЯ ФОРМУЛ
В СИМВОЛЬНОМ МОДЕЛИРОВАНИИ:
ОТ РЕЗУЛЬТАТА К ИСХОДНОЙ ФОРМУЛЕ
А.Б. Годлевский, С.В. Потиенко
Институт кибернетики имени В.М. Глушкова НАН Украины,
03680, Киев, проспект Академика Глушкова, 40.
Тел.: (+38) (044) 526 0058.
stepan@iss.org.ua
В символьном моделировании транзиционных систем аналогом их состояний являются логические формулы над множеством
атрибутов. Правила переходов исходной системы служат основой для построения моделирующих правил, которые действуют на
формульных состояниях и определяют переход от исходного состояния к последующему или предшествующему ему состоянию.
Предикатный трансформер – это алгоритм, моделирующий переходы в пространстве формульных состояний. В работе описан
обратный предикатный трансформер, отличительной чертой которого является то, что моделируемые им переходы допускают как
операторы присваивания над простыми и составными структурами данных (массивами и списками), так и констрейнты, задающие
изменения атрибутов в неявном виде.
Logical formulas over attributes set are analog of system states in symbolic modeling of transition systems. Transition rules of source system
are the base for building of modeling rules which operate on formula state and define transition from source state to the next or previous state.
Predicate transformer is an algorithm which models transitions in the formula state space. We describe backward predicate transformer which
has distinguishing feature that modeled transitions allow as assignment operators over simple and complex data structures (arrays and lists) as
constraints which define attribute changes implicitly.
Введение
Трансформация формул под действием операторов программ активно изучалась в рамках подхода к
верификации программ, предложенного Флойдом [1] и развитого затем Хоаром [2]. Рассматривались
логические формулы над переменными программы, привязываемые к ее состоянию и описывающие свойства
программы при передаче управления в это состояние. По отношению к оператору, исполняемому в заданном
состоянии программы, требовалось определить, каким соотношениям будут удовлетворять значения
переменных после его выполнения, или, в символьной постановке, каким образом оператор трансформирует
логическую формулу, имевшую место до его выполнения. Эта задача известна как построение постусловия по
заданному условию и оператору. Двойственной к ней является задача построения предусловия по условию и
оператору, когда исходная формула выражает соотношение переменных после выполнения оператора и
требуется определить, каким соотношениям должны удовлетворять переменные программы, чтобы этот
оператор приводил к заданной формуле. Сложность этих задач по трансформации формул зависела как от
языка представления формул, в частности используемых в них предикатов и структур данных, так и от
семантики самих операторов.
Интерес авторов к задаче трансформации формул связан с технологией проверки свойств программ на
моделях (model checking), когда для исследования достижимых состояний применяется символьное
моделирование, позволяющее существенно редуцировать пространство поиска. В данной работе
рассматривается обратное моделирование, которое соответствует построению предусловий. Рассмотрение
проводится в рамках модели, заданной набором базовых протоколов [3], что, как формализм, соответствует
правилам перехода в транзиционных системах. Предлагаемый здесь механизм преобразования формул будем
называть (обратным) предикатным трансформером.
Отличительной чертой постановки являются язык формул и семантика трансформаций. Формулы
рассматриваются как над простыми атрибутами, так и над атрибутами функционального типа (массивами) и
списками. Допускаются чтение, добавление и удаление элементов как по отношению к началу, так и к концу
каждого списка. Базовые протоколы синтаксически состоят из двух частей, предусловия, определяющего
возможность применения к состоянию среды, и постусловия, которое определяет преобразование атрибутов
1
.
Постусловия задают высокоуровневые преобразования данных и включают в себя три компоненты,
исполняемые параллельно: присваивания, обработку списков и констрейнты, специфицирующие часть
атрибутов. Таким образом, изменение одних атрибутов явно задается присваиваниями, для других же их новые
значения задаются неявно в виде ограничений.
Работа является развитием [4], здесь устранены имевшиеся ошибки, детально рассмотрен алгоритм
отождествления аргументов функциональных символов и расширено описание примеров.
1
Мы используем термин атрибут системы вместо термина переменная программы, а также термины пред-
условие и постусловие как структурные составляющие базового протокола, но не как результаты трансфор-
мации одних формул в другие.
mailto:stepan@iss.org.ua
Формальні методи програмування
364
1. Обозначения
На каждом шаге моделирования известно текущее состояние среды (на первом шаге известно начальное
состояние). Применимые в этом состоянии протоколы модифицируют состояние согласно своим постусловиям.
Каждый из одновременно применимых протоколов создает новую ветвь в дереве поведения системы.
Описанные далее пред- и постусловия, а так же формулы, определяющие состояния среды, могут
содержать связанные переменные (x). Здесь они явным образом не участвуют, так как обрабатываются в
других процедурах и в данный алгоритм изменений не вносят.
Пред- и постусловие каждого базового протокола представляется в таком виде:
– предусловие: A(r,l,s,z);
– постусловие: B(r,l,s,z) = R(r,l,s,z) U(l,r,s,z) C(r,s).
Здесь:
– l – вектор списковых атрибутов;
– r,s,z – вектора атрибутов и атрибутных выражений, кроме списков;
– A(r,l,s,z) и C(r,s) – формулы базового языка; A может содержать операторы доступа к спискам
get_from_head, get_from_tail и empty, С – нет;
– U(l,r,s,z) – конъюнкция операторов обновления списков l;
– R(r,l,s,z) – конъюнкция присваиваний новых значений атрибутам r, может содержать операторы доступа к
спискам get_from_head и get_from_tail в правых частях:
– (r1(r,l,s,z) := t1(r,l,s,z)) (r2(r,l,s,z) := t2(r,l,s,z)) …;
– ri(r,s,z) := ti(r,s,z) – присваивания после подстановки элементов списков вместо операторов доступа
(get_from_head(l), get_from_tail(l)); подстановки осуществляются после восстановления списков (см. раз-
дел 2), так как здесь нужно использовать "старые" значения;
– z – вектор переменных, отсутствующих в атрибутных выражениях верхнего уровня формулы C(r,s)
постусловия и левых частей присваивания.
Таким образом, r – это левые части присваиваний и функциональные выражения, которые рекурсивно
зависят от левых частей. Они представляют собой атрибутные выражения, значения которых меняются
присваиваниями. Значения s могут измениться недетерминированным образом, поскольку входят в условие С.
Значения выражений из z не меняются.
Пусть E и E' – формулы, определяющие символьные состояния среды, которые, в свою очередь,
покрывают множества конкретных состояний. Для простоты, формулы E будем называть состояниями. Они
представляются в таком виде:
– E = D(r,s,z) L(r,l,s,z),
– E' = D'(r,s,z) L'(r,l,s,z),
где
– D(r,s,z), D'(r,s,z) – формулы базового языка [4] (могут содержать связанные переменные);
– L(r,l,s,z), L'(r,l,s,z) – списковые равенства вида:
- (l1 = list(h1(r,s,z), h2(r,s,z), ..., Nil; q1(r,s,z), q2(r,s,z), ..., Nil)) …
… (l2 = list(c1(r,s,z), c2(r,s,z), ..., Nil)) …;
- hi(r,s,z), qi(r,s,z), и ci(r,s,z) – выражения соответствующего типа;
- списки могут содержать абстрактную (неизвестную) часть, как l1, или иметь конкретную длину, как l2.
Базовый протокол применим на состоянии среды E, если формула E A(r,l,s,z) не ложна. Применимый
базовый протокол осуществляет переход:
E E' .
Во время прямого моделирования известно состояние E, с помощью прямого предикатного трансформера
необходимо найти состояние E':
E' = pt( E A(r,l,s,z), B(r,l,s,z) ).
Во время обратного моделирования известно состояние E', с помощью обратного предикатного
трансформера необходимо найти состояние E:
E = pt
-1
( E', A(r,l,s,z), B(r,l,s,z) ).
2. Формульная часть
Рассмотрим формульную часть постусловия B(r,l,s,z) без обновления списков:
R(r,l,s,z) C(r,s).
Постусловие кроме операторов присваивания и обновления списков содержит формулу базового языка.
Обновление списков производится по правилам, описанным далее. Рассмотрим влияние полученной формулы
C(r,s) на формулу D.
Операторы присваивания и формула C(r,s) изменяют формулу состояния среды как описано в прямом
предикатном трансформере [4]. Далее речь идет об обратном моделировании.
Условие валидности постусловия определяется такой формулой: R(r,s,z) C(r,s). Условие применимости
– D' R C. Так же необходимо учитывать списки: если в части постусловия U есть операторы add_to_head
или add_to_tail, то соответствующие списки не должны быть пустыми в L' (но могут быть абстрактными).
Пусть эти условия выполняются.
Формальні методи програмування
365
Построим формулу
D(r,l,s,z) = (y,u) ( D'(u,l,y,z) u = t(r,l,s,z) C(u,y) P(r,s,z,y) ) A(r,l,s,z),
P(r,s,z,y) = P1(r,s,z,y) P2(r,s,z,y) ... (1)
Здесь y и u – векторы связанных переменных, введенных для обозначения значений, которые имеют
атрибуты s и r до выполнения обратного трансформера.
Выше упоминалось, что r, s, z – векторы атрибутов и атрибутных выражений не списковых типов, т.е.
простых типов – числовые (целые и действительные), перечислимые, символьные, а так же функциональных
типов. Массивы могут рассматриваться как функциональные типы с целочисленными или перечислимыми
параметрами, целочисленные ограничены размерностями массива. Эти ограничения имеют вид неравенств:
i 0 i < N, где i – индексное выражение, N – размерность массива, и должны учитываться при проверке
выполнимости формул. Если один атрибут функционального типа встречается в пред- или постусловии и/или
состоянии E' (включая списки) более одного раза, должны быть рассмотрены все комбинации возможных
отождествлений его аргументов. Формула Pi(r,s,z,y) определяет одну из таких возможностей. Так как P – это
дизъюнкция всех Pi, состоящих из равенств и неравенств аргументов, то она тождественно равна 1. Т.е.
присутствие P в формуле (1) не влияет на состояние среды, описываемое этой формулой.
Рассмотрим метод построения P с учетом такого ограничения: разрешается только один уровень
вложенности аргументов, т.е. выражение в аргументе не может содержать функциональных символов
(например, a(a(x)) запрещено).
Сначала рассмотрим все аргументы функциональных символов, входящих в B и E'. Предусловие А пока
не рассматриваем, так как оно остается неизменным. Обозначим эти аргументы как
k
iw , где индекс k
обозначает место аргумента и тип содержащего функционального символа, индекс i – перечисляет все
вхождения этого аргумента. Например, для формулы g(a,b,c) > g(d,e,f), обозначения аргументов будут
выглядеть так: fwewdwcwbwaw 3
2
2
2
1
2
3
1
2
1
1
1 ,,,,, .
1. Сделаем подстановки атрибутов из r на t(r,l,s,z) согласно присваиваниям в постусловии, атрибутов из s
– на связанные переменные yi, так как новое состояние E' содержит новые значения всех атрибутов.
2. Построим отождествление P как дизъюнкцию всех возможных комбинаций Pi равенств и неравенств
аргументов. Для этого надо раскрыть скобки в формуле: ( , , ) ( ).k k k k
i j i j
i j
P i j k w w w w
3. Далее, к первой части формулы (1) без предусловия A будем применять функцию отождествления
(F(r,s,z), Pi(r,s,z)) для каждого Pi. Определим функцию (F, Pi) как замену в формуле F аргументов
функциональных символов, исходя из равенств, присутствующих в Pi. Замена происходит следующим образом:
пусть в F есть два функциональных символа a(x) и a(v), а в Pi есть равенство x = v. В случае, когда оба символа
a(x) и a(v) r, отождествлять x = v нельзя, так как в постусловии запрещено делать более одного присваивания
одному атрибуту. Если же один из символов a(x) r, то v заменить на x, что бы остались вхождения
атрибутного выражения из r, вместо которого потом можно будет подставить t(…). Если же a(x) s, a(v) z, то
будет аналогичная замена, останутся вхождения атрибутного выражения из s, вместо которых потом можно
будет подставить подкванторные переменные y. Если символы a(x) и a(v) из одного вектора s или z, то можно
сделать любую замену. Обозначим: Di' = (D', Pi), Ci = (C, Pi).
См. примеры в разделе 4.
Если формула D(r,s,z) ложна, то данный базовый протокол не мог быть применен и соответствующая
ветвь поведения не рассматривается.
Таким образом:
pt
-1
( D'(r,s,z) , A(r,l,s,z), B(r,l,s,z) ) =
= y
i
( Di'(t(r,l,s,z),y,z) Ci( t(r,l,s,z),y) Pi(r,s,z,y) ) A(r,l,s,z).
3. Восстановление списков
Операторы обновления списков U(r,l,s,z) изменяют списковые равенства в состоянии среды:
pt(L(r,l,s,z), U(r,l,s,z)) = L'(r,l,s,z),
pt
-1
(L'(r,l,s,z), A(r,l,s,z), U(r,l,s,z)) = L(r,l,s,z).
U(r,l,s,z) содержит операторы add_to_tail(l, f(r,s,z)), add_to_head(l, f(r,s,z)), remove_from_tail(l, f(r,s,z)),
remove_from_head(l, f(r,s,z)).
L(r,l,s,z) содержит равенства вида (см. раздел 1):
l = list(h1(r,s,z), , hm(r,s,z), Nil; q1(r,s,z), , qn(r,s,z), Nil).
Голова или хвост списка могут быть пусты, тогда l = list(Nil; q1(r,s,z), …, Nil) или l = list(h1(r,s,z), …, Nil;
Nil) соответственно.
Полностью абстрактный список содержит только неизвестную часть: l = list(Nil; Nil).
Восстановление списков и генерация списковых равенств L(l,r,s,z) осуществляется по правилам:
1) для оператора add_to_tail(l,f(r,s,z)):
Формальні методи програмування
366
– если L'(l,r,s,z) содержит равенство l = list(h1(r,s,z), , Nil; q1(r,s,z), , qn(r,s,z), Nil), то применяем
remove_from_tail(l);
тогда L(l,r,s,z) содержит равенство
y ( l = list(h1(t(r,s,z),y,z), , Nil; q1(t(r,s,z),y,z), , qn-1(t(r,s,z),y,z), Nil) );
в формулу F необходимо добавить равенство f(r,s,z) = qn(t(r,s,z),y,z);
– если L'(l,r,s,z) содержит равенство l = list(h1(r,s,z), , Nil; Nil), то неизвестная часть остается неизвестной;
тогда L(l,r,s,z) содержит равенство y ( l = list(h1(t(r,s,z),y,z), , Nil; Nil) );
2) для оператора add_to_head(l,f(r,s,z)):
– если L'(l,r,s,z) содержит равенство l = list(h1(r,s,z), …, Nil; q1(r,s,z), …, Nil), то применяем remove_from_head(l);
тогда L(l,r,s,z) содержит равенство
y ( l = list(h2(t(r,s,z),y,z), …, Nil; q1(t(r,s,z),y,z), …, Nil) );
в формулу F необходимо добавить равенство f(r,s,z) = h1(t(r,s,z),y,z);
– если L'(l,r,s,z) содержит равенство l = list(Nil; q1(r,s,z), …, Nil), то неизвестная часть остается неизвестной;
тогда L(l,r,s,z) содержит то же равенство y ( l = list(Nil; q1(t(r,s,z),y,z), …, Nil) );
3) для оператора remove_from_tail(l):
– пусть L'(l,r,s,z) содержит равенство l = list(h1(r,s,z), …, Nil; q1(r,s,z), …, qn(r,s,z), Nil);
вводим новую переменную v и применяем add_to_tail(l,v);
тогда L(l,r,s,z) содержит равенство
(y,v) ( l = list(h1(t(r,s,z),y,z), …, Nil; q1(t(r,s,z),y,z), …, qn(t(r,s,z),y,z), v, Nil) ).
4) для оператора remove_from_head(l):
– пусть L'(l,r,s,z) содержит равенство l = list(h1(r,s,z), …, Nil; q1(r,s,z), …, Nil);
вводим новую переменную v и применяем add_to_head(l,v);
тогда L(l,r,s,z) содержит равенство
(y,v) ( l = list(v, h1(t(r,s,z),y,z), …, Nil; q1(t(r,s,z),y,z), …, Nil) ).
У списков конкретной длины отсутствует неизвестная часть, правила обновления применяются те же.
Необходимо лишь отдельно рассмотреть случай, когда состояние E' содержит пустой список l = list(), а
постусловие базового протокола оператор add_to_tail(l) или add_to_head(l). Тогда этот протокол не мог быть
применен и соответствующая ветвь поведения не рассматривается.
pt
-1
( D'(r,s,z) L'(l,r,s,z), A(r,l,s,z), B(r,l,s,z) ) =
= D(r,l,s,z) y(L(l,t(r,s,z),y,z)) M(r,s,z).
Здесь M(r,s,z) – конъюнкция равенств, добавленных во время восстановления списков для операторов
add_to_tail и add_to_head.
4. Примеры с отождествлением аргументов
Пример 1. Столбцы в таблице описывают: (А) – предусловие, (R) – оператор присваивания, (C) –
условие, E’ – состояние среды, (Р) – соотношения между атрибутами, задающие конкретные формулы. Будем
говорить о «новых» и «старых» значениях атрибутов, полагая, что новые – результат применения базового
протокола к состоянию со старыми значениями. Однако, поскольку мы рассматриваем обратное
моделирование, то исходными для предикатного трансформера будут «новые» значения, а результатом
моделирования будет реконструкция «старых» значений, точнее тех соотношений, которые должны были
выполняться, чтобы базовый протокол был применимым.
Трасформацию условий будем представлять в виде таблицы, в столбцах которой будут соответственно
представлены: (А) – предусловие базового протокола, (R) – оператор присваивания, (U) – оператор обновления
списков, (E) исходное условие, (Р) равенства и их отрицания, описывающие разные случаи отождествления
аргументов функциональных выражений. Условимся также новые значения в таблицах выделять жирным
шрифтом. В рассматриваемом примере отсутствуют операторы обработки списков, а сам пример задается в
первой строке табл. 1. К «новым» значениям относятся: формула E’ и значения атрибутов a[i] и a[k],
формируемые постусловием базового протокола. Заметим, что в (R) и (C) обновляются только значения
массива, но не значения индексов у элементов этого массива.
Описание среды для этого примера будет следующим: массив a из трех элементов, целочисленные
атрибуты i, j и k. Интерпретация строк таблицы (кроме первой, в которой представлено описание базового
протокола и исходного условия) соответствует разбору разных случаев интерпретации исходной формулы E.
Эти случаи соответствуют разным соотношениям индексов i, j и k, представленным в столбце Р.
Каким образом «новые» значения должны подставляться в формулу E? Во-первых, если i=k, то
результат присваивания может подставляться в условие (С); во-вторых, поскольку значение индекса i не
менялось ни в присваивании R, ни в условии С, то в формуле E новым значением элемента a[i] будет значение
a[k]+1, где a[k] – это старое значение; в-третьих, a[j] может заменяться на a[k] при j=k, но не на a[i] (поскольку
из i=j должно следовать a[i]=a[j], но эти элементы в E не совпадают).
Итак, относительно значений индексов, встречающихся в выражениях для элементов массива допустимы
три комбинации, перечисленные в столбце Р. Для каждого значения в столбце Р осуществляем под-
становку в С и E’.
Формальні методи програмування
367
Таблица 1
(A) Precond (R) Assign (C) Cond (U) List E’ (Р) Cases
а[i]+a[j]+a[k]=5 a[i]:=a[k]+1 a[k]<=0 a[i]>a[j]
a[i]=a[k]+1 a[k]<=0 a[k]+1>a[j] ik, jk, ij
a[i]=a[k]+1 a[k]<=0 a[k]+1>a[k] ik, j=k, ij
a[i]=a[k]+1 a[k]+1<=0 a[k]+1>a[j] i=k, ij
Рассмотрим подробно случай, когда ik, jk, ij, соответствующий второй строке табл. 1. Новые значения
элементов a[i] и a[k] определяются присваиванием, для a[i], и условием для a[k]. При этом новое значение a[i]
выражается как a[k]+1 через старые, а новое значение a[k] от старых не зависит и лишь ограничено сверху
числом 0. Значение a[j] базовым протоколом не изменяется. Поэтому неравенство a[i]>a[j], присутствующее в
E для новых значений трансформируется в a[k]+1>a[j] для старых, неравенство a[k]<=0 заменяется на формулу
(Exist y)(y<0), отражающую замену a[k] связанной переменной у. С учетом формулы предусловия,
выполнимость которой есть условие применимости базового протокола, предикатный трансформер строит
формулу
(Exist y)(а[i]+a[j]+a[k]=5) &((y<0)&(a[k]+1>a[j])&(ij)&(ik)&(jk),
соответствующую данному соотношению индексов.
Обратим внимание на последнюю строку табл. 1 (случай i=k & ij). Поскольку i=k, то в условие (С)
подставляется значение a[i], порождаемое присваиванием, и условие (С) трансформируется к виду a[k]+1<0,
которому должны удовлетворять старые значения атрибутов. С учетом всех трех случаев формула будет иметь
вид:
(Exist y)(а[i]+a[j]+a[k]=5)&(ij)&(
(y<0)&(a[k]+1>a[j])&(ik)&(jk) |/
(y<0)&(a[k]+1>y) &(ik)&(j=k) |/
(a[k]+1<0)&(a[k]+1>a[j]) & (i=k)
)
Замечание 1. Предикатный трансформер, должен был бы вначале построить полную дизъюнкцию из 5
членов, включая 2 члена, когда i=j, а затем удалить эти два члена должна уже процедура проверки
выполнимости, которая встроена в трансформер, чтобы проверять не тривиальность результата и упрощать
результирующую формулу.
Замечание 2. Предусловие базового протокола попадает в формулу в неизменном виде и может
измениться только в результате упрощений, если раскрыть скобки дизъюнкции.
Замечание 3. Если присваивания базового протокола будут изменять атрибуты, входящие в индексные
выражения, то выражения в столбце (Р) определяющие частные случаи трансформации формулы, могут зависеть
не только от атрибутов типа r,s,z, но и от связанных переменных, которыми заменяются атрибуты типа s.
Пример 2. Особенность этого примера в том, что здесь присутствует обработка списков. Обратим
внимание на то, что формула E характеризует значение элемента, лежащего в списке.
Таблица 2
(A) Precond (R) Assign (C) Cond (U) List E (Р) Cases
а[i]+a[j]=5 a[i]:=get_from_h
ead(l)
a[j]<=0 remove_from_he
d(l)
a[i]+a[j]>0 & &
a[2]>=1 &
l=list(a[2],Nil)
а[i]+a[j]=5 a[i]:=v a[j]<=0 (Exist v) (
a[i]+a[j]>0 &
a[2]>=1 &
l=list(v,a[2],Nil) )
a[i]=v a[j]<=0 (Exist v) (
a[2]+a[j]>0 &
a[2]>=1 &
l=list(a[2],a[2],Nil) )
i=2, ij
a[i]=v a[j]<=0 (Exist v) (
v+a[j]>0 & a[2]>=1
& l=list(v,a[2],Nil) )
i2, ij
Как и ранее, в первой строке табл. 2 представлены исходные данные для предикатного трансформера. Во
второй строке описано преобразование, связанное с восстановлением списка l , и в третьей и четвертой
рассматриваются два нетривиальных случая трансформации условия.
Формальні методи програмування
368
В первую очередь восстановим список l, добавив в него некий элемент v (переменную, связанную
экзистенциальным квантором). После чего заменим оператор чтения из головы списка значением этого
элемента. В результате, задача трансформера преобразуется к следующей:
присваивание из (R) заменяется на a[i]:=v;
оператор восстановления списков из U удаляется (как уже промоделированный);
список l в E увеличивается путем дописывания в его голову нового элемента.
Этой задаче соответствует вторая строка табл. 2.
Атрибуты типа r и s как и ранее – это a[i] и a[j]. Сопоставляться между собой могут их индексы и индекс
2 элемента из списка l. Рассмотрим возможные случаи.
Случай j=2 отбрасываем как невыполнимый, поскольку значение a[2], большее 1, несовместимо с
ограничением a[j]<=0.
Случай i=2 позволяет определить значение связанной переменной v как a[2].
Случай i2 и i=j отбрасываем как невыполнимый, связанная переменная v должна быть не больше 0
(условие для a[j]), а тогда сумма a[i]+a[j], равная 2v, должна быть одновременно не больше 0 и больше 0
(условие a[i]+a[j]>0 из E).
Если теперь в (С) и E’ обновленный атрибут a[j] заменить связанной переменной у, то итоговая формула
принимает вид:
(Exist v,у)( (а[i]+a[j]=5 & ij & у<=0 & a[2]>=1) &
(a[2]+у>0 & l=list(a[2],a[2],Nil) |/ v+у>0 & l=list(v,a[2],Nil) )
В эту формулу вошли равенство из предусловия (А), ограничение ij, которое верно для всех
выполнимых случаев, условие у<=0 из (С), неравенство a[2]>=1 из E, которое вынесено за скобки как общее
для обоих дизъюнктов.
Выводы
В данной работе рассмотрена техника обратного символьного моделирования, которая используется для
решения задач верификации систем базовых протоколов. Описан алгоритм обратного предикатного
трансформера, моделирующего переход транзиционной системы от заданного формульного состояния к
предшествующему ему состоянию. Этот алгоритм ориентирован на такие типы данных как integer, real
и enumerated, а также на структуры функциональных и списочных типов данных. Обратный трансформер
рассматривают как оператор, который по заданной формуле строит новую, определяющую класс состояний
системы, из которых возможен переход, совершенный под действием заданного базового протокола.
Следующий важный этап в этой работе, который еще требует своего завершения, состоит в том, чтобы
доказать свойство идеальности описанного предикатного трансформера. Суть этого свойства состоит в
установлении адекватности формульной модели по отношению к конкретной модели, в которой состояния
транзиционной системы задаются наборами значений всех своих атрибутов. Иными словами s – состояние,
удовлетворяющее формульному состоянию E, s – состояние, к которому применим базовый протокол и
которое он переводит в s, то нужно показать, (1) что s будет удовлетворять формульному состоянию E, которое
порождает трансформер, и (2) для каждого состояния s, удовлетворяющего формуле Е, существует состояние s,
удовлетворяющее E, и такое, что базовый протокол переводит s в s.
1. Floyd R. W. «Assigning Meaning to Programs», in Proceedings of Symposium on Applied Mathematics, Vol. 19, J.T. Schwartz (Ed.), A.M.S.,
1967. – Р. 19–32.
2. Hoare C. A. R. «An axiomatic basis for computer programming». Communications of the ACM, 12(10): 576–580, 583 October 1969.
3. Летичевский А.А., Капитонова Ю.В., Волков В.А., Летичевский А.А. (мл.), Баранов С.Н., Котляров В.П., Вейгарт Т. Спецификация
систем с помощью базовых протоколов // Кибернетика и системный анализ – № 4. –2005.
4. Потиенко С.В. Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами // Проблеми
програмування. – 2008. – № 4. – С. 39–45.
http://laser.cs.umass.edu/courses/cs521-621.Spr06/readlings/Floyd.pdf
http://ru.wikipedia.org/wiki/1967
http://ru.wikipedia.org/wiki/C._A._R._Hoare
http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf
http://ru.wikipedia.org/w/index.php?title=Communications_of_the_ACM&action=edit&redlink=1
|
| id | pp_isofts_kiev_ua-article-923 |
| institution | Problems in programming |
| keywords_txt_mv | keywords |
| language | Russian |
| last_indexed | 2026-06-02T01:01:19Z |
| publishDate | 2026 |
| publisher | PROBLEMS IN PROGRAMMING |
| record_format | ojs |
| resource_txt_mv | ppisoftskievua/f2/03a9aa5aa339bd756762be011d50dff2.pdf |
| spelling | pp_isofts_kiev_ua-article-9232026-06-01T06:02:58Z Backward transformation of formulas in symbolic modeling: from the result to the source formula Обратная трансформация формул в символьном моделировании: от результата к исходной формуле Godlevsky, A.B. Potienko, S.V. UDC 519.686.2 УДК 519.686.2 Logical formulas over attributes set are analog of system states in symbolic modeling of transition systems. Transition rules of source system are the base for building of modeling rules which operate on formula state and define transition from source state to the next or previous state. Predicate transformer is an algorithm which models transitions in the formula state space. We describe backward predicate transformer which has distinguishing feature that modeled transitions allow as assignment operators over simple and complex data structures (arrays and lists) as constraints which define attribute changes implicitly.Problems in programming 2010; 2-3:363-368 В символьном моделировании транзиционных систем аналогом их состояний являются логические формулы над множеством атрибутов. Правила переходов исходной системы служат основой для построения моделирующих правил, которые действуют на формульных состояниях и определяют переход от исходного состояния к последующему или предшествующему ему состоянию. Предикатный трансформер – это алгоритм, моделирующий переходы в пространстве формульных состояний. В работе описан обратный предикатный трансформер, отличительной чертой которого является то, что моделируемые им переходы допускают как операторы присваивания над простыми и составными структурами данных (массивами и списками), так и констрейнты, задающие изменения атрибутов в неявном виде.Problems in programming 2010; 2-3:363-368 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2026-06-01 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/923 PROBLEMS IN PROGRAMMING; No 2-3 (2010); 363-368 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2010); 363-368 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2010); 363-368 1727-4907 ru https://pp.isofts.kiev.ua/index.php/ojs1/article/view/923/992 Copyright (c) 2026 PROBLEMS IN PROGRAMMING |
| spellingShingle | UDC 519.686.2 Godlevsky, A.B. Potienko, S.V. Backward transformation of formulas in symbolic modeling: from the result to the source formula |
| title | Backward transformation of formulas in symbolic modeling: from the result to the source formula |
| title_alt | Обратная трансформация формул в символьном моделировании: от результата к исходной формуле |
| title_full | Backward transformation of formulas in symbolic modeling: from the result to the source formula |
| title_fullStr | Backward transformation of formulas in symbolic modeling: from the result to the source formula |
| title_full_unstemmed | Backward transformation of formulas in symbolic modeling: from the result to the source formula |
| title_short | Backward transformation of formulas in symbolic modeling: from the result to the source formula |
| title_sort | backward transformation of formulas in symbolic modeling: from the result to the source formula |
| topic | UDC 519.686.2 |
| topic_facet | UDC 519.686.2 УДК 519.686.2 |
| url | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/923 |
| work_keys_str_mv | AT godlevskyab backwardtransformationofformulasinsymbolicmodelingfromtheresulttothesourceformula AT potienkosv backwardtransformationofformulasinsymbolicmodelingfromtheresulttothesourceformula AT godlevskyab obratnaâtransformaciâformulvsimvolʹnommodelirovaniiotrezulʹtatakishodnojformule AT potienkosv obratnaâtransformaciâformulvsimvolʹnommodelirovaniiotrezulʹtatakishodnojformule |