TermWare3 – term rewriting system, based on context-term calculus
In this paper, the design of the TermWare-3 rewriting system which is built on the ground of reflective calculus of context term is considered. In the calculus of the context term, term structure contains not only tree, but a reference to an internal context and matching constrains (external context...
Збережено в:
| Дата: | 2019 |
|---|---|
| Автори: | , |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
Інститут програмних систем НАН України
2019
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/349 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-349 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/ce/473f1afe6c4a054cfa7eb4288a1a0ace.pdf |
| spelling |
pp_isofts_kiev_ua-article-3492024-04-28T11:00:17Z TermWare3 – term rewriting system, based on context-term calculus TermWare-3 – система переписывания термов, основанная на исчислении контекстов TermWare3 – система переписування термів, заснована на контекстному численні Shevchenko, R.S. Doroshenko, A.Yu. automated software design; programming languages; term rewriting; type systems; code analysis; TermWare UDC 004.4'24 автоматизированное проектирование программ; языки программирования; переписывание термов; системы типов; анализ кода; TermWare УДК 004.4'24 автоматизація розробки програмного забезпечення; мови програмування; переписування термів; системи типів; алгебра типів; аналіз коду; termware УДК 004.4'24 In this paper, the design of the TermWare-3 rewriting system which is built on the ground of reflective calculus of context term is considered. In the calculus of the context term, term structure contains not only tree, but a reference to an internal context and matching constrains (external context). This allows to embed operation of name resolving into the mathematical semantics of the term rewriting. The elements of algebra are multiterms, which complement context terms by constructions of arrows, universal matching pattern and consistent set. This allows to emulate substitutions of typed variables in the terms of multiterm algebra. Also, the method of effective rule dispatch is described. Example of usage term rewriting system for checking of smart-contract properties, with automatic transformation of expression between representation in terms of Scala algebraic types and TermWare-3 context terms is shown. Problems in programming 2019; 1: 48-58 В статье описывается конструкция системы переписывания термов TermWare-3, построенной на основе рефлексивного исчисления контекстных термов, когда структура терма включает в себя дополнительно к дереву терма еще внутренний контекст и ограничения на сопоставление (внешний контекст). Это позволяет погрузить операции разрешения имен в математическую семантику переписывающих правил. Элементами алгебры являются мультитермы, которые дополняют контекстные термы конструкциями стрелок, универсальным образцом сопоставления и непротиворечивых множеств. Это позволяет эмулировать подстановку типизированных переменных в рамках алгебры мультитермов. Также описывается метод эффективной диспетчеризации выбора правил. Приводится пример применения системы переписывающих правил для анализа смарт-контрактов вместе с автоматическим преобразованием выражения между системами на основе алгебраических типов Scala и контекстными термами.Problems in programming 2019; 1: 48-58 У статті описується конструкція системи переписування термів TermWare-3, що побудована на основі рефлексивного числення контекстних термів, коли структура терму включає до себе, окрім дерева, ще й внутрішній контекст та обмеження на співставлення при застосуванні (зовнішній контекст), що дозволяє занурити операції розв’язування імен в математичну семантику переписувальних правил. Описується метод ефективної диспетчеризації вибору правил, а також автоматичне перетворення виразів між системами на основі алгебраїчних типів мови Scala та контекстними термами.Problems in programming 2019; 1: 48-58 Інститут програмних систем НАН України 2019-03-26 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/349 10.15407/pp2019.01.048 PROBLEMS IN PROGRAMMING; No 1 (2019); 48-56 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 1 (2019); 48-56 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 1 (2019); 48-56 1727-4907 10.15407/pp2019.01 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/349/357 Copyright (c) 2019 PROBLEMS IN PROGRAMMING |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2024-04-28T11:00:17Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
automated software design programming languages term rewriting type systems code analysis TermWare UDC 004.4'24 |
| spellingShingle |
automated software design programming languages term rewriting type systems code analysis TermWare UDC 004.4'24 Shevchenko, R.S. Doroshenko, A.Yu. TermWare3 – term rewriting system, based on context-term calculus |
| topic_facet |
automated software design programming languages term rewriting type systems code analysis TermWare UDC 004.4'24 автоматизированное проектирование программ языки программирования переписывание термов системы типов анализ кода TermWare УДК 004.4'24 автоматизація розробки програмного забезпечення мови програмування переписування термів системи типів алгебра типів аналіз коду termware УДК 004.4'24 |
| format |
Article |
| author |
Shevchenko, R.S. Doroshenko, A.Yu. |
| author_facet |
Shevchenko, R.S. Doroshenko, A.Yu. |
| author_sort |
Shevchenko, R.S. |
| title |
TermWare3 – term rewriting system, based on context-term calculus |
| title_short |
TermWare3 – term rewriting system, based on context-term calculus |
| title_full |
TermWare3 – term rewriting system, based on context-term calculus |
| title_fullStr |
TermWare3 – term rewriting system, based on context-term calculus |
| title_full_unstemmed |
TermWare3 – term rewriting system, based on context-term calculus |
| title_sort |
termware3 – term rewriting system, based on context-term calculus |
| title_alt |
TermWare-3 – система переписывания термов, основанная на исчислении контекстов TermWare3 – система переписування термів, заснована на контекстному численні |
| description |
In this paper, the design of the TermWare-3 rewriting system which is built on the ground of reflective calculus of context term is considered. In the calculus of the context term, term structure contains not only tree, but a reference to an internal context and matching constrains (external context). This allows to embed operation of name resolving into the mathematical semantics of the term rewriting. The elements of algebra are multiterms, which complement context terms by constructions of arrows, universal matching pattern and consistent set. This allows to emulate substitutions of typed variables in the terms of multiterm algebra. Also, the method of effective rule dispatch is described. Example of usage term rewriting system for checking of smart-contract properties, with automatic transformation of expression between representation in terms of Scala algebraic types and TermWare-3 context terms is shown. Problems in programming 2019; 1: 48-58 |
| publisher |
Інститут програмних систем НАН України |
| publishDate |
2019 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/349 |
| work_keys_str_mv |
AT shevchenkors termware3termrewritingsystembasedoncontexttermcalculus AT doroshenkoayu termware3termrewritingsystembasedoncontexttermcalculus AT shevchenkors termware3sistemaperepisyvaniâtermovosnovannaânaisčisleniikontekstov AT doroshenkoayu termware3sistemaperepisyvaniâtermovosnovannaânaisčisleniikontekstov AT shevchenkors termware3sistemaperepisuvannâtermívzasnovananakontekstnomučislenní AT doroshenkoayu termware3sistemaperepisuvannâtermívzasnovananakontekstnomučislenní |
| first_indexed |
2024-09-16T04:08:35Z |
| last_indexed |
2024-09-16T04:08:35Z |
| _version_ |
1818568269071646720 |
| fulltext |
Інструментальні засоби та середовища програмування
© Р.С. Шевченко, А.Ю. Дорошенко, 2019
48 ISSN 1727-4907. Проблеми програмування. 2019. № 1
УДК 004.4'24 https://doi.org/10.15407/pp2019.01.048
Р.С. Шевченко, А.Ю. Дорошенко
TERMWARE-3 – СИСТЕМА ПЕРЕПИСУВАННЯ ТЕРМІВ,
ЗАСНОВАНА НА КОНТЕКСТНОМУ ЧИСЛЕННІ
У статті описується конструкція системи переписування термів TermWare-3, що побудована на основі
рефлексивного числення контекстних термів, коли структура терму включає до себе, окрім дерева, ще й
внутрішній контекст та обмеження на співставлення при застосуванні (зовнішній контекст), що дозво-
ляє занурити операції розв’язування імен в математичну семантику переписувальних правил. Опису-
ється метод ефективної диспетчеризації вибору правил, а також автоматичне перетворення виразів між
системами на основі алгебраїчних типів мови Scala та контекстними термами.
Ключові слова: автоматизація розробки програмного забезпечення, мови програмування, переписуван-
ня термів, системи типів, алгебра типів, аналіз коду, termware.
Вступ
Системи перепиcування та логічно-
го виводу давно застосовуються для різних
задач. Перша версія системи TermWare
описана у статті [1] і з’явилась у 2003 році
як система термів, заснована на безтипо-
вому переписуванні термів [2], що допов-
нена взаємодією з базою фактів. Ця систе-
ма довела свою ефективність для широко-
го кола задач [3, 4]. Друга версія, була за-
снована на тому ж математичному апараті,
але на відміну від першої версії мала ін-
ший спосіб реалізації. Тоді як у першій ве-
рсії рекурсивні алгоритми обходу дерева
інтерпретувались за допомогою рекурсив-
них Java методів, то в другій – за допомо-
гою вбудованого нерекурсивного інтерп-
ретатора, що не використовує вбудований
стек JVM для обходу дерев. Це дозволило
застосування TermWare-2 в індустріальних
задачах, де можна було подати кожен файл
нетривіальної Java-програми як один вели-
кий терм і виконувати перетворення, що
потребують обходу всіх файлів проекту. У
такому вигляді система TermWare-2 засто-
совується і нині [3, 4].
Система TermWare-3 (і побудована
на її основі мова програмування Vavilon),
з одного боку, зберігають основні риси
TermWare-2, як вбудованої високорівневої
бібліотеки, з іншого – додають нові мож-
ливості застосування примітивів контекс-
тного числення [5]. Як і попередня версія,
TermWare-3 – це бібліотека, що містить
в собі операції роботи з термами та мож-
ливість створення та застосування пере-
писувальних правил до об’єктів користу-
вача.
1. Основні конструкції TermWare-3
У цьому розділі ми приведемо осно-
вні конструкції числення контекстних тер-
мів та наведемо спосіб їх представлення у
вигляді Scala-конструкцій TermWare-3.
Нехай T – множина термів, що
складається з множини константних сим-
волів 𝐶, з виділеною підмножиною атомів
𝐴 ⊂ C та функціональних термів 𝐹 ⊂
⊂ 𝐴 . Побудуємо на її основі множину кон-
текстних мультитермів 𝐶𝑇(𝑇), що буде
включати в себе:
константи 𝐶𝑖, 𝑖 ∈ 𝐼:
- константні терми, що не є ато-
мами, представлені як трейти (характерис-
тики) PrimitiveTerm[T], де T – це приміти-
вний тип Scala, a PrimitiveTerm[T]; існує
неявне перетворення між примітивними
типами Scala та PrimitiveTerm;
- атоми, що представлені як
трейти AtomTerm; існує неявне перетво-
рення між Scala символами та AtomTerm;
функціональні терми 𝑓𝑖(𝑡1, …
… , 𝑡𝑛) ∈ 𝐹, 𝑖 ∈ 𝐼. TermWare-3 підтримує
більш застосовану до способу мислення
розробників концепцію структурних тер-
мів 𝑓𝑖(𝑛1 = 𝑡1, … , 𝑛𝑚 = 𝑡𝑚), де n1, n2… nm –
імена (атоми), t1, ..., tm – мультитерми;
cтруктурні терми, що є абстракцією ви-
клику функції, що в сучасних мовах може
http://dx.doi.org/10.7124/bc.000027
Інструментальні засоби та середовища програмування
49
включати іменовані параметри та значення
за замовчуванням. Ці структурні терми
представлені як вигляди трейта Struc-
turedTerm. Існує реалізація цього трейта
для case-классів, головне в цьому трейті –
операція іменування;
перетворення (стрілки) 𝑡1 → 𝑡2:
- реалізація Scala надає трейт
ArrowTerm; його основна функціональ-
ність – можливість виділення лівої та пра-
вої частини перетворення, жодна з яких не
є пустою;
- внутрішній контекст context(a,b)
або 𝑎@𝑏, що можна читати як a в контекс-
ті b, де a та b – будь-які терми (в форму-
лах іноді використовується нотація 𝑎𝑏); в
Scala реалізація будь-якого ординарного
терма може мати внутрішній контекст
(можливо пустий), для операцій з ним іс-
нують методи, описані в трейті
ContextBase;
зовнішній контекст a -: b що
можна описати як: “a при умові контексту
b”. Будемо також інколи використовувати
позначення b:-a, тобто, контекст має бути
ближче до двокрапки. Ідея в тому, що при
використаннi a -: b як паттерна, його мо-
жна співставляти (як a) лише у випадку,
коли контекст співставлення сумісний з b
(детальніше описуеться при опису уніфі-
кації). В реалізації Termware-3 будь-який
терм має зовнішній контекст, який за за-
мовченням є ‘*’ – універсальним мульти-
терм, що сумісний з будь-яким термом;
множинні мультитерми (або
or-вирази); {𝑡1 … 𝑡𝑛} (або 𝑡1 or 𝑡2 … or
𝑡𝑛 ) – можна розглядати як просто множи-
ну ординарних термів. Пуста множина
еквівалентна виділеному терму Empty-
Term. В TermWare-3 множинний мульти-
терм представлений трейтом OrSet, що на
додаток до звичайних операцій над тер-
мами, дає доступ до вибірки та переліку
елементів. Також, над термами визначена
операція or.
сумісні множинні мультитерми
(або and-вирази); ≪ 𝑡1, … 𝑡𝑛 ≫ (або
𝑡1𝑎𝑛𝑑 𝑡2, 𝑎𝑛𝑑 … 𝑡𝑛). Вони відрізняються від
or-термів тим, що мають бути сумісні між
собою. Формальне визначення сумісності
наведемо після переліку термів, неформа-
льно – два терми сумісні, якщо це стрілки
з різними лівими частинами або один з них
є множинним термом або вони однакові.
Пустий множинний мультитерм є універ-
сальним термом. TermWare-3 надає трейт
AndSet та операцію and над мульти-
термами;
послідовність альтернатив
𝑡1| 𝑡2| … | 𝑡𝑜𝑡ℎ𝑒𝑟, або t1 orElse t2 orElse … tn ,
при співставленні результатом є перша
можлива альтернатива. TermWare-3 надає
операцію orElse над термами;
захищений терм: if(guard, t), де
співставлення виконується лише якщо ви-
раз guard інтерпретується в true у логічній
системі, що може задаватись як параметр
системи. У TermWare є трейт IfTerm;
порожній мультитерм ∅, який
можна інтерпретувати як “пустий мно-
жинний мультитерм”, що у TermWare-3
представлений об’єктом EmptyTerm;
універсальний мультитерм ∗,
який можна інтерпретувати як “сумісний з
будь-яким мультитермом”, представленим
об’єктом StarTerm.
Користуючись базисом цих елемен-
тів, можна емулювати конструкції станда-
ртної логіки. Так, наприклад, підстановка
може бути представлена як сумісний терм:
≪ 𝑥1 → 𝑡1, … 𝑥𝑛 → 𝑡𝑛 ≫ , де 𝑥𝑖 – атоми з
іменами, що відповідають іменам змінних,
а 𝑡𝑛 – результати. Додавання ще одного
елемента або створить нову сумісну підс-
тановку, або перетворить підстановку у
пустий терм, що буде свідчити про
неуспішність операції.
Вільні змінні з іменами 𝑥𝑖 можуть
бути емульовані як атоми з іменами та
підстановкою, що перетворює ці імена в
обмеження. Вираз
𝑓(𝑥1, 𝑥2)@{ 𝑥1 → ∗ , 𝑥2 →∗ }
відповідає вільним змінним 𝑥1 та 𝑥2 без
обмежень. Для змінних з обмеженнями
використовуються захищені терми:
𝑓(𝑥1, 𝑥2)@{𝑥1 → 𝑖𝑓 (𝑡ℎ𝑖𝑠 < 2) ∗, 𝑥2 →
𝑖𝑓 (𝑖𝑠𝑆𝑡𝑟𝑖𝑛𝑔(𝑡ℎ𝑖𝑠)) →∗ }.
Інструментальні засоби та середовища програмування
50
При співставленні x1, this поміщається у
зовнішній контест терму і вираз this < 2
інтерпретується у базовій логіці.
Природним чином эмулюється по-
няття типу: (x:T) це скорочення для захи-
щеного терму if (T.resolve(check),this). Та-
ким чином, тип у TermWare-3 є доведен-
ням властивості безтипового виразу. Тобто
останній вираз можна переписати як:
𝑓(𝑥1, 𝑥2)@{𝑥1 → 𝑖𝑓 (𝑡ℎ𝑖𝑠 < 2) ∗, 𝑥2
→ 𝑖𝑓 (𝑡ℎ𝑖𝑠: 𝑆𝑡𝑟𝑖𝑛𝑔) →∗ }.
Саму систему переписувальних правил та-
кож можна представити у вигляді терму:
це буде сумісна множина стрілок
≪ 𝑝1 → 𝑡1, … 𝑝𝑛 → 𝑡𝑛 ≫,
де 𝑝1, … 𝑝𝑛 – паттерни, 𝑡1, … 𝑡𝑛 – відповідні
підстановки. Як видно, підстановка є час-
тинним випадком систем правил, і там
основним є правило підстановки одного
правила:
𝑎𝑝𝑝((𝑥 → 𝑦), 𝑧) = {
𝑠𝑢𝑏𝑠𝑡(𝑦, 𝑢𝑛𝑖𝑓𝑦(𝑥, 𝑧)),
𝑢𝑛𝑖𝑓𝑦(𝑥, 𝑧) ≠ ∅
∅, 𝑢𝑛𝑖𝑓𝑦(𝑥, 𝑧) = ∅.
,
Місце в системі правил – визначається
операцією вибору. В такому представ-
ленні, переписувальні правила мають бу-
ти когерентними (тобто не суперечити
одне одному).
Ще один варіант представлення –
впорядкований набір правил, що може бу-
ти представлений за допомогою переліку
альтернатив. Такий терм має вигляд:
𝑥1 → 𝑡1| 𝑥2 → 𝑡2| … | 𝑥𝑛 → 𝑡𝑛.
Зазначимо, що якщо терми з більш-
специфічним паттерном знаходяться рані-
ше більш загальних, то ці два представ-
лення еквівалентні [5].
За браком місця не будемо наводи-
ти повний опис формальної системи. Най-
більш близький опис є у [5, 6]. Там подана
попередня формалізація, де немає різниці
між сумісними та несумісними множинами
термів.
2. Імплементація
Стандартний метод представлення чис-
лення в Scala – моделювання основних
конструкцій у вигляді ієрархїї case-класів
та побудова алгебри операцій над цими
case-класами як окремого об’єкта. В
TermWare-3 прийнятий інший підхід, що
на перший погляд вступає у протиріччя з
загальноприйнятим функціональним сти-
лем. А саме, основні конструкції є трейта-
ми, що допускають різні реалізації, а алге-
бра операцій представлена як методи цих
трейтів. Основна причина такого дизайну
– можливість ефективної реалізації.
Як приклад, подивимось на про-
блему диспетчерізації правил. Нехай у нас
є терм x та система переписувальних пра-
вил:
≪ 𝑝𝑖 → 𝑦𝑖 … ≫.
Як знайти правило з лівою частиною, що
сумісне з x? Якщо ми використовуємо
систему case-класів, то нам потрібно або
організовувати пошук лівої частини в
послідовності правил, що не є ефектив-
ним методом, або явно перетворювати си-
стему правил в оптимізоване представ-
лення, що ускладнює зовнішній інтерфейс
бібліотеки [7].
Наприклад, розглянемо наступну
систему правил:
(
𝑓(𝑥,𝑔(𝑦),𝑥)→𝑝1(𝑥,𝑦)|
𝑓(𝑥,𝑥,𝑥)→𝑝2(𝑥)
𝑓(𝑥,𝑦,𝑥)→𝑝3(𝑥,𝑦)
𝑔(𝑦)→𝑦
𝑥→𝐴 )
@(𝑥→∗
𝑦→∗
).
При співставленні раціонально
тримати в пам’яті не список стрілок, а
структуру, що застосована для швидкого
метчінгу, показану на наступному рисун-
ку.
Тут кожна вершина використовує
табличний пошук (за арністю або ім’ям
головного терма), далі виконується співс-
тавлення з типовим термом, і якщо воно
Інструментальні засоби та середовища програмування
51
Рисунок. Структура для швидкого метчінгу
правильне – то проводиться остаточно пе-
ревірка, якщо ні – співставлення продов-
жується з “fallback”-вершини, перехід до
якої показано пунктирною стрілкою.
Якщо взяти, наприклад, набір даних
p(1,1,1), то для визначення потрібного
правила досить двох вибірок з таблиці: пе-
рший за арністю, другий – за іменем, а по-
тім можна відразу переходити до правила
𝑥 → 𝐴; 𝑓(1,1,1), що потребує трьох співс-
тавлень. У існуючій реалізації, відбуваєть-
ся спочатку табличний пошук за арністю,
далі – табличний пошук за іменами і лише
на третьому (передостанньому) рівні – по-
вне співставлення. Теоретично ще можли-
во ввести кількісну оцінку складності спів-
ставлення та будувати структуру, що буде
мінімізувати цю оцінку на наборі вхідних
даних.
3. Приклад застосування
Наведемо приклад застосування
аналізу контексту, на прикладі імплемен-
тації перевірки контрактів.
Нехай у нас є опис контракту на
мові Solidity [8], що є типовим представ-
ником об’єктно-орієнтованих мов з вкла-
деними областями визначення. Для прос-
Інструментальні засоби та середовища програмування
52
тоти викладу, ми не розглядатимемо фазу
синтаксичного аналізу та припустимо, що
об’єктом нашого розгляду є представлення
Solidity AST у вигляді глибоко вбудовано-
го (deep embedding) [9] виразу Scala.
Контракт на Solidity фактично є
описом актора, що активується при надхо-
дженні транзакції, де може бути вказано
додаткове повідомлення, що декодується у
виклик методу. Він включає у себе опис
стану актора, набір можливих функцій та
вихідних випадків (events), що доступні
для спостереження, разом з визначенням
необхідних структур даних та модифікато-
рів.
На Scala це описується наступною
ієрархією:
case class Contract(
name: String,
contractMember: Seq[ContractMember])
sealed trait ContractMember
case class VarDef[T](
name:String,
dataType: DataType[T],
scope: Scope,
location: DataLocation) extends ContractMem-
ber
sealed trait FunctionLikeMember extends Con-
tractMember
case class ConstructorMember(
params: Map[String,VarDef[_]],
statements: IndexedSeq[Statement]
) extends FunctionLikeMember
case class FunctionMember(
params: Map[String,VarDef[_]],
statement: IndexedSeq[Statement])
Тут DataType – це тип даних, що може бу-
ти або вбудованим, або побудованим ко-
ристувачем:
sealed trait DataType[T]
sealed trait Primitive[T] extends DataType[T]
case class IntPrimitive(value: Int) extends Primi-
tive[Int]
case class AddressPrimitive(value: Long)
extends Primitive[Long]
……..
case class Struct(fields:
Map[String,DataType[_]])
extends
DataType[Map[String,DataType[_]]]
case class Mapping[
K:Primitive,
V:DataType](value:Map[K,V])
extends
DataType[Map[K,V]]
……
case class SArray[T:DataType](
value: IndexedSeq[T]
) extends DataType[IndexedSeq[T]]
і нарешті Statement – це може бути виклик
методу, присвоювання значення, ініціалі-
зація локальної змінної тощо. Скорочено
це можно проілюструвати наступним фра-
гментом:
case class MethodCall[O,T](obj: Expr[O],
params: LExpr[_]) extends Expr[T]
case class VarName[T](name:String) extends
LExpr[T]
case class Assignment[T](left: LExpr[T] ,expr:
Expr[T]) extends Statement
case class VarInit[T](name:String,
dateType:DataType[T],
initExpr: RExpr[T]) extends Statement
case class IfStatement(condition:RExpr[Boolean],
Інструментальні засоби та середовища програмування
53
ifTrue: Statement,
ifFalse: Statement) extends Statement
Як бачимо, вся програма представлена
як алгебраїчна структура даних. В
TermWare-3 реалізовано автоматичне пере-
творення екземплярів алгебраїчних типів
у терми: все що потрібно, це проімпорту-
вати DSL та викликати розширений метод
перетворення:
val programTerm = ast.toTerm()
Але за замовчуванням, структура AST бу-
де перенесена в таку ж структуру терму
без побудови контекста. Для того, щоб
показати, що деякі частини належать до
контексту, потрібно вказати відображення
поля в розташування підтерму (що може
бути або в підтермі, або в контексті):
implicit object ContractContextPlacement
extends AsContext[
Seq[ContractMember],
Symbol,
ContractMember]{
override def map(in: Seq[ContractMember]):
Try[Map[Symbol, ContractMember]] = {
Try {
in.map(m => (Symbol(m.name), m)).
groupBy(_._1).
mapValues {
s =>
if (s.tail.nonEmpty) {
throw new IllegalArgumentException(
"duplicate name ${s.head._1}")
} else {
s.head._2
}
}
}
}
override def unmap(in: Map[Symbol, Con-
tractMember]): Try[Seq[ContractMember]] = {
Success(in.values.toSeq)
}
}
І схоже перетворення потрібно вказати для
VarDef, щоб визначення змінної потрап-
ляло у контекст блоку. Як бачимо, задача
цього перетворення – перетворення терму
на маппінг, що згодом перетворюється на
набір впорядкованих даних. Також зазна-
чимо використання типу Symbol як ключа
відображення, замість String. Це зроблено
тому, що String за замовченням відобража-
ється у PrimitiveTerm[String] а Symbol – в
AtomTerm.
Також має сенс імена змінних та ча-
стини селектори теж представляти як ато-
ми:
implicit def varNameFieldMapping[T] =
new AsFieldMapping[VarName[T],Symbol] {
override def map(in: VarName[T]):
Try[Symbol] = Success(Symbol(in.name))
override def unmap(in: Symbol):
Try[VarName[T]] = Suc-
cess(VarName(in.toString()))
}
Тепер programTerm, представлений як
терм, в контексті якого знаходяться визна-
чення (тут ми для простоти оминули дода-
вання стандартних елементів програми, що
визначені в специфікації Solidity). Ми мо-
жемо використовувати навігацію за сим-
волами: x.resolve(name) видасть нам визна-
чення імені.
Розглянемо, для прикладу, програ-
му перевірки (чекер) так званої
«reentrance» [10] – помилки в контрактах,
коли контракт робить транзакцію, не змі-
нюючи свого стану. Саме ця вразливість
була використана у відомому зломі DAO
[11].
Приклад проблеми такого роду мо-
жна побачити в наступному коді:
contract Example {
mapping (address=>uint) balances;
….
function add() {
balances[sender.address] += msg.valuel
Інструментальні засоби та середовища програмування
54
}
function withdraw(uint amount) {
if (balances[sender_address] > amount) {
sender.address.send(amount);
balances[sender.address] -= amount;
}
}
Тут у функції withdrаw, метод send
викликається до модифікації balanc-
es[sender.address]. Оскільки send – це фак-
тично виклик функції прийому платежа в
іншому контракті, то інший контракт може
викликати функцію withdrаw ще раз, до
того як поверне керування, і отримати ще
один трансфер на свою адресу.
Система правил для знайдення цієї
вразливості може виглядати так:
StateVars(statements, history) -> {
statements . (seq(head,tail) ->
IfStatement(expr,ifTrue,ifFalse) ->
Stat-
eVars(seq(ifTrue,tail)) &&
Stat-
eVars(seq(ifFalse,tail)) head
|
StateVars(tail, StateVars(head) + history)
)
Assignment(left,expr) -> StateVars(left)
MethodCall(account,'send,params)
if (resolve(account).type == address &&
history.isEmpty)
-> Violation("reentrance-bug")
|
MethodCall(obj,metod,params) ->
let v = re-
solve(obj).resolce(method).statements
StateVars(tail,StateVars(v) + history)
Тут пропущені деталі, які не впли-
вають на алгоритм, такі як вказання набо-
ру змінних. Цю систему правил ми маємо
викликати до кожного методу. Тобто, ми
проводимо рекурсивний спуск за послідо-
вністю виразів, введемо в history множину
і коли потрапляємо на виклик методу send,
перевіряємо, що множина змін не є пус-
тою.
Якщо ми зустріли виклик об’єкта в
програмі, то додаємо до множини змін йо-
го слід (трейс).
Висновки
Отже, в даній роботі представлена сис-
тема TermWare-3 на основі імплементації
контекстного числення термів. Це дозво-
ляє застосувати методи переписувальних
правил до великих систем і подавати
зв’язки між різними частинами системи у
явному вигляді за допомогою розв’язання
імен (резолвінгу).
Подальші кроки, що планується здійс-
нити в цьому напрямку, це:
- адаптація застосування Term-
Ware-3 у прикладних проектах;
- інтеграція з аналізаторами мов
програмування Java та C, таким чином,
щоб існувала можливість міграції систем
на основі TermWare-2 на нову платформу;
- імплементація відображення
системи типів Scala на TermWare-3 з тим
щоб отримати типобезпечне вбудовування
в Scala;
- побудова та аналіз ефективних
імплементацій базових операцій.
Література
1. Shevchenko R., Doroshenko A. Managing
Business Logic with Symbolic Computation.
Information Systems Technology and
Applications: Proc. 2-nd Intern. Conf.
ISTA'2003, June 19–21, 2003. Kharkiv,
Ukraine. P. 143–152.
2. Marc Bezem, Jan Willem Klop, Roel de
Vrijer ("Terese"), Term Rewriting Systems
("TeReSe"), Cambridge University Press,
2003.
Інструментальні засоби та середовища програмування
55
3. Doroshenko A., Shevchenko R. A rewriting
framework for rule-based programming dy-
namic applications. Fundamenta Informati-
cae. 2006. Vol. 72, N 1–3. P. 95–108.
4. Eugene Tulika, Anatoliy Doroshenko,
Kostiantyn Zhereb. Using Choreography of
Actors and Rewriting Rules to Adapt Legacy
Fortran Programs to Cloud Computing. June
2017. Communications in Computer and
Information Science.
5. Шевченко Р.С., Дорошенко А.Е. η-
исчисление – реалистичная формализация
класса переписывающих систем. Проблеми
програмування. 2011. № 2. С. 3–11.
6. Шевченко P.C. Числення контекстних тер-
мів для систем переписування. Проблеми
програмування. 2018. № 2–3. С. 21–30.
7. Шевченко Р. Про імплементацію систем
контекстних термів. Winter InfoCom Ad-
vanced Solutions. 2018. 41 с.
8. Ethereum Foundation. The solidity contract-
oriented programming language.
https://github.com/ethereum/solidity.
9. Jeremy Gibbons and Nicolas Wu. Folding
domain-specific languages: deep and shallow
embeddings (functional Pearl). In Proceedings
of the 19th ACM SIGPLAN international
conference on Functional programming (ICFP
'14). 2014. ACM, New York, NY, USA.
P. 339–347.
10. Loi Luu, Duc-Hiep Chu, Hrishi Olickel,
Prateek Saxena, and Aquinas Hobor. Making
Smart Contracts Smarter. In Proceedings of
the 2016 ACM SIGSAC Conference on
Computer and Communications
Security (CCS'16). ACM, New York, NY,
USA. P. 254–269.
11. "Report of Investigation Pursuant to Section
21(a) of the Securities Exchange Act of 1934:
The DAO" (PDF). Securities and Exchange
Commission. July 25, 2017.
References
1. Shevchenko R., Doroshenko A. Managing
Business Logic with Symbolic Computation.
Information Systems Technology and
Applications: Proc. 2-nd Intern. Conf.
ISTA'2003, June 19–21, 2003, Kharkiv,
Ukraine. P. 143–152.
2. Marc Bezem, Jan Willem Klop, Roel de
Vrijer ("Terese"), Term Rewriting Systems
("TeReSe"), Cambridge University Press,
2003, ISBN 0-521-39115-6.
3. Doroshenko A., Shevchenko R. A rewriting
framework for rule-based programming dy-
namic applications. Fundamenta Informaticae.
2006. Vol. 72, N 1–3. P. 95–108.
4. Eugene Tulika, Anatoliy Doroshenko,
Kostiantyn Zhereb. Using Choreography of
Actors and Rewriting Rules to Adapt Legacy
Fortran Programs to Cloud Computing. //
June 2017. Communications in Computer
and Information Science, DOI: 10.1007/978-
3-319-69965-3_5
5. Shevchenko R.S., Doroshenko A.Y. η-
calculus – Realistic Formalization of a Class
of Rewriting Systems. Problems of Program-
ming. 2011. N 2. P. 3–11.
6. Shevchenko R.S. A Calculus of Context
Terms for Rewriting Systems. Problems of
Programming. 2018. N 2–3. P. 21–30.
7. Shevchenko R. On Implementation of Term
Systems. Winter InfoCom Advanced Solu-
tions, 2018. 41 p.
8. Ethereum Foundation. The solidity contract-
oriented programming language.
https://github.com/ethereum/solidity.
9. Jeremy Gibbons and Nicolas Wu. Folding
domain-specific languages: deep and shallow
embeddings (functional Pearl). //In
Proceedings of the 19th ACM SIGPLAN
international conference on Functional
programming (ICFP '14). 2014. ACM, New
York, NY, USA, 339-347. DOI:
https://doi.org/10.1145/2628136.2628138
10. Loi uu, Duc-Hiep Chu, Hrishi Olickel,
Prateek Saxena, nd Aquinas Hobor. Making
Smart Contracts Sarter. In Proceedings of the
2016 ACM SIGSAC Conference on
Computer and Communications
Security (CCS '16). ACM, New York, NY,
USA, 254-269. DOI:https://doi.org/
10.1145/2976749.2978309
11. "Report of Investigation Pursuant to Section
21(a) of the Securities Exchange Act of 1934:
The DAO" (PDF). Securities and Exchange
Commission. July 25, 2017.
Одержано 08.02.2019
Інструментальні засоби та середовища програмування
56
Про авторів:
Шевченко Руслан Сергійович.
Підприємець.
Кількість наукових публікацій в
українських виданнях – 13.
Кількість наукових публікацій в
зарубіжних виданнях – 5.
http://orcid.org/0000-0002-1554-2019,
Дорошенко Анатолій Юхимович,
доктор фізико-математичних наук,
професор, завідувач відділу
теорії комп’ютерних обчислень,
професор кафедри автоматики та
управління в технічних системах
НТУУ “КПІ імені Ігоря Сікорського ”.
Кількість наукових публікацій в
українських виданнях – понад 150.
Кількість наукових публікацій в
зарубіжних виданнях – понад 50.
Індекс Хірша – 5.
http://orcid.org/0000-0002-8435-1451,
Місце роботи авторів:
ПП “Руслан Шевченко”.
E-mail: ruslan@shevchenko.kiev.ua
Інститут програмних систем
НАН України,
03187, м. Київ-187,
проспект Академіка Глушкова, 40.
Тел.: (044) 526 3559.
E-mail: doroshenkoanatoliy2@gmail.com
|