1 Введение 3
1.1 Вычисление Хора . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.1.1 Тройка Хора . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.1.2 Логический вывод . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.1.3 Автоматизация логического вывода . . . . . . . . . . . . . . . . . . . . . . . . . 25
1.1.4 Альтернативные подходы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1.2 Объектные вычисления . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
1.3 Модели динамических куч . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
1.3.1 Преобразование в стек . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
1.3.2 Анализ образов . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
1.3.3 Ротация указателей . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
1.3.4 Файловая система . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
1.4 Побочные области . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
1.4.1 Анализ псевдонимов . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
1.4.2 Сбор мусора . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
1.4.3 Интроспекция кода . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
1.5 Существующие среды . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

2 Проблемы динамической памяти 66
2.1 Мотивация . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
2.2 Проблемы в связи с корректностью . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
2.3 Проблемы в связи с полнотой . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
2.4 Проблемы в связи с оптимальностью . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77

3 Выразимость формул куч 79
3.1 Граф над кучами . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
3.2 Предикаты . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89

4 Логическое программирование и доказательство 99
4.1 Пролог как система логического вывода . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
2

4.2 Логический вывод как поиск доказательства . . . . . . . . . . . . . . . . . . . . . . .
4.3 Совместимость языков . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.4 Представление знаний . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.5 Архитектура системы верификации . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.6 Объектные экземпляры . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

5 Ужесточение выразимости куч 132
5.1 Мотивация . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.2 Многозначимость операторов . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.3 Ужесточение операторов . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.4 Классовый экземпляр как куча . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.5 Частичная спецификация куч . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.6 Обсуждения . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

6 Автоматическая верификация с предикатами 156
6.1 Сжатие и развёртывание . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.2 Предикатное расширение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.3 Предикаты как логические правила . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.4 Интерпретация предикатов над кучами . . . . . . . . . . . . . . . . . . . . . . . . . .
6.5 Перевод правил Хорна . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.6 Синтаксический перебор как верификация куч . . . . . . . . . . . . . . . . . . . . . .
6.7 Свойства . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.8 Реализация . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.9 Выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

7 Заключение 198

Список сокращений 204

Список терминов 205

Литература 221

Список определений 246

Список иллюстраций 249

Приложение: Предметный указатель 252

Во введении (первая глава) для построения таксономии проблем и подходов к верифи- кации динамической памяти предлагается «лестница качества»: Корректность < Полно- та < Оптимальность. Полнота включает в себя автоматизацию и тотальность. Оптималь- ность использования ресурсов включает в себя например быстродействие, безопасность и т.д. Аксиоматическая семантика, основанная на правилах формой A ⇒ B, вводится как основа вычисления Хора, чьи компоненты содержат пред- и постусловие P и Q, а так- же программный оператор C некоторого императивного языка программирования. Эти три компоненты называются «тройка Хора». Минимальный объем логических правил включает правила «усиления предусловия» (STRONGPE) и «ослабление постусловия» (WEAKPOST). Минимальный объем операторных правил включает правила «присво- ения» (ASN), «цикла» (LOOP) и «оператор последовательности» (SEQ). Инвариант цикла является единой формулой условия, которая содержит все переменные меняющи- еся в теле цикла и которая на протяжении выполнения верна. Тройка Хора записывается как {P}C{Q}, и если не гарантировано совершение C, то тройка является импликацией {P}C{Q} → (C ̸= ⊥) ∧ Q. Задача верификации заключается в том, чтобы проверить, согласно данному набо- ру правил, выводим ли результат лишь при использовании данных логических правил и аксиом |=B. Структура вывода описывается деревом. Центральная проблема вывода, это эффективный поиск дерева вывода. Главный вопрос заключается в том, как лучше представить все компоненты троек Хора, правила вывода и как лучше подобрать входной императивный язык программирования для того, чтобы верификация была корректной и полной. Далее, сходимость является важным свойством, когда необходимо гарантиро- вать, что верификация продолжит вывод. Обсуждается, что корректность и полнота в зависимости от набора правил или входного языка программирования, часто исключают друг друга. Любое утверждение в вычислении Хора является логическим предикатом. Предикат решает данное утверждение об состоянии вычисления верное или нет. Представляются три основные принципа вывода в классической логике: дедукция, индукция и абдукция. Вычисление Хора имеет пределы. Статические и глобальные переменные, со-процедуры, продолжения и ограничения в связи с параметрами приводятся в качестве примеров. В некоторых работах верификация динамически выделенных переменных оценивается как крайне трудная. Проводится анализ существующих ограничений, их теоретическая и практическая роль, а также анализируется система обозначений. Оценивается важность включения описаний в более универсальный императивный язык программирования, ко- торый близок к Си со структурами/объектными экземплярами. Устанавливаются главные критерии: (1) простое состояние и трансформации програм- мы должны сопоставляться простым описанием, (2) простые доказательства должны простым образом доказываться, простые отрицательные доказательства должны про- стым образом отрицаться, (3) «островные решения» часто не такие хорошие, как ка- жется на первый взгляд, а наоборот, усложняют и ограничивают более эффективные подходы. Многие авторы в различных ситуациях и по различным причинам замечают, что выразимость – это одна из наиболее сильных преград. «Coq», «verifast» и другие ассистенты доказательств используют ряд тактик для уско- рения нахождения доказательства. В качестве типов спецификации ассистенты основаны на типизированных лямбда-вычислениях второго порядка T→. Бо ́льшая гибкость ожи- λ2 дается, если далее типы параметризовать, т. е. предложить T→. Проблема отсутствия ав- λ3 томатизированного свертывания и развертывания индуктивных определений при дока- зательстве кажется существенной преградой. Решению этой проблемы посвящена часть данной работы. Логическая формула в предикатной логике первого порядка определятся как: Φ ::= true | false | x | REL(f(x)) | P(x) | ¬Φ | Φ ◦ Φ | ∀x.Φ[x] | ∃x.Φ[x] где f описывает функтор, REL является некоторой реляции, а ◦ бинарный логический оператор. Выявляется необходимость отделения различных теорий от структурных теории ве- рификации, например, когда речь идет о равенствах целых чисел для достижения эф- фективного решения вместо раздувания все новых и/или сложных правил. Всязи с этим ставится вопрос об упрощении остальных компонент – программных операторов и опи- сание состояния, как основной подход. Было показано, что доказательство динамической кучи может быть эффективно реа- лизовано с помощью логического программирования, т.е. с помощью процедур и лемм, автоматизированного метода вывода абстрактных предикатов, термового представления куч и ужесточения пространственных операторов, и т.д. Процесс верификации определяется как статический метод проверки спецификации. Устанавливается разница в подходах к проверке типов: Проверка типов по Хиндлей- Милнеру: ⊢Γ e : t Вывод типов (type inference), дано: e: найти: t ? Проблема содержимого (inhabitant problem), дано: t, problem), дано: {P}, {Q}, найти: C . найти: e? Сравнив имеющиеся объектные вычисления по Абади-Карделли и Абади-Лейно, ко- торые оба не включают указатели, в прототипе предложено и реализовано расширение основаное на объектном вычислении Абади-Карделли, включая указатели и псевдонимы вместе с классами. Вводятся и утверждаются некоторые конвенции об объектах, которые полезны для исчисления динамических куч. Запрещаются встроенные объекты. Одному указателю положено ссылаться на один объект не более одного раза. Разные указатели могут ссы- латься на любые объекты, в том числе, ни на какой, либо все на один. В отличие от структур, объект имеет жизненный цикл, который далее совместим с моделью куч. По- дробно обсуждается разница между объектами типизацией и спецификацией. Тип клас- са определяется всеми полями как: Tj → Tj+1 → ··· → Tk. По Абади-Лейно объектный экземпляр строится полями и методами: [fi = xi,i = 1..n,mj = ψ(yj)bj,j = 1..m] Недо- статком является потенциально рекурсивное определение содержимого. Вследствии в общности обработка становится трудной. Проверка принадлежности классового (под-)типа может быть определена по- элемент- носледующимобразом:A<:A′ ⇔[fi :Ai,i=1..n+p,mj :Bj,j=1..m+q]=A ∧[fi : Ai = 1..n,mj : Bj,j = 1..m] = A′,p,q ∈ N0 Показано, что чем сильнее разделение ответственности между объектами, тем меньше имеется связей/зависимостей между указателями, тем проще спецификация динамиче- ской памяти, тем меньше имеется исключений, тем полнее и выше качество верифи- кации. Устанавливается аналогия с метрикой МакКейба о сложности графов потоков. Если при верификации обнаруживаются лишние элементы, то спецификация, либо не полная, либо ошибка в программе только что обнаружена. Динамические проблемы не всегда возможно преобразовать в стек из-за неопределенности размера стека и фрагмен- тации. Альтернативные подходы описания графа кучи включают в себя анализ образов, вы- числение регионов, перемещение в стек, или преобразование связей памяти в файловую систему. Например, для сборки мусора общее количество пишущих операций, и связи между ячейками в динамической памяти очень важны для быстрого доступа. На примере подхода «ротация указателей» можно вывести, что компактность записи куч не достаточна. Необходимо исключать неожиданные изменения в описаниях куч, вычисление Хора: ⊢Γ {P}C{Q} ≡ B Логический Вывод (inference), дано: B, Γ, найти: B ⊢Γ An,0.. ⊢Γ An−1,.. ⊢Γ A0,... Проверка типов (type checking), дано: e, t: проверить: ⊢Γ e : t? Проверка доказательства (proof checking), где Ai,j аксиома тройка, Ai,j правило: B ⊢Γ An,0.. ⊢Γ An−1,.. ⊢Γ A0,.., дано: все. Проблема содержимого (inhabitant это можно соблюдать с помощью требования о локальности, которые в основном вво- дились логикой распределённой памяти и усовершенствуются при строгих операторах делимости кучи, а также модуляризируются с помощью абстрактных предикатов. Представлены и сравнены альтернативные модели представления динамической па- мяти, прежде всего — это преобразование в стек, анализ образов и представление куч в файловой системе. Выявлены существенные ограничения альтернативов, а также ради проверки на возможные недостатки и противоречия рассмотрены и косвенные области работы с динамической памятью — это подходы анализа псевдонимов, сбор мусора и интроспекция кода в динамической памяти. Вторая глава уточняет выбранные проблемы из первой главы для верификации ди- намической памяти. Приводятся мотивирующие примеры и анализ проблем, даётся тео- ретическое и практическое оправдание актуальности этих проблем. Обсуждаются причины, примеры проблем, которые могут возникать и их необходи- мо локализовать: (a) доступ к недоступной памяти, висячие указатели, (б) доступ к не инициализированной памяти, (в) нехватка динамической памяти при востребовании, (г) снижение быстродействия, (д) утечка памяти. В (a) адрес не был выделен, либо ссылка осталась, а содержимое содержит что-то другое/ничего. В (д) происходит переопреде- ление содержимого указателя. Сценарий (в) осуществляется почти всегда после долгого времени запуска и остается без подозрений долгое время. Предлагается первое неформальное определение общего графа кучи: содержит указа- тели, которые ссылаются на элементы в динамической памяти. Памятные ячейки могут быть сложными. Граф строится/меняется пошагово согласно выполнению программных операторов. В отличие от стека, куча (динамическая память) неорганизованна и связи между элементами определяются явным образом, а занесение и утилизация проводится специальными операторами. В работе с динамической памятью проблемы классифицируются и приоризируются на корректность, полноту, быстродействие и адэкватность выбранных представленний. Связанные между этими свойствами критерии критично обсуждаются и формулируются по важности для верификации динамической памяти. Основные существующие теоре- тические принципы критично анализируются, а их практическое значение оценивается и выделяется. Третья глава посвящается выразимости кучевого представления. Блок видимости определенный для локальных переменных различается от динамически выделенных пе- ременных. Соответствие между началом определения переменной и концом видимости блока отсутствует. Граф кучи меняется по одному элементу в операторах, при этом, из- менение должно происходить локально. Опасность «далекой манипуляции» нужно вклю- чать как усложняющий фактор. Из-за локальности регулярные выражения полностью исключаются. Фрейм определяет динамические кучи до и после вызова процедуры: {P }C {Q} {P ⋆ R}C{Q ⋆ R} Граф кучи определяется как тройка (V, E, L × V ∪ {nil}), где V множество вершин, E множество граней и L множество наименований указателей. Указатель ссылается, либо на v ∈ V , либо на nil, т.е. не инициализирован. Для представления множеств V и E имеются несколько возможностей, чьи преимущества и недостатки обсуждаются. Выбор делается на представление близкое к «логике распределённой памяти». Обыск и обнару- жение соседей производится с O(n). Анализируя данные определения куч, выходит, что существующие определения проводятся только строго говоря, множественной формой «кучи», единичная форма так и отсутствует. Результатом этого недостатка и неточности в определении влечёт за собой неопределённость, в следствии чего, анализ куч услож- няется значительно из-за необходимости полного анализа контекста данной части кучи. Нетрудно убедиться в том, что явное оправдание даётся лишь за счёт более сложного подхода. На первый взгляд не очевидное замечание приводит к попытке определить граф кучи впервые как: Направленный и просто связанный граф, вершины чьи расположены в адресном про- странстве динамической части оперативной памяти. Циклы разрешаются. С каждой вершины отходит максимально одна грань, исключением являются объектные эк- земпляры, поля чьи могут быть указателями. Каждая вершина графа присвоена к некоторому определенному базисному или классному типу, который определят размер вершины. Вершина имеет адрес в динамической памяти и имеет содержимое совмести- мого значения. Адреса всех вершин различаются, пересечение вершин исключается. Более формальный в логике распределенной памяти основанное определение далее будет далее рассматриваться в пятом разделе на основе соотношений между кучами. Обсуждается необходимость ввода предикатов для описания куч. Предикаты парамет- ризируются общими переменными символами для более широкого круга применимости. В отличие от имеющихся подходов, динамические переменные не ограничиваются блоком видимости. Предикаты могут использоваться и ссылаться на любые другие предикаты, в том числе на самих себя. Так как внутренние объекты запрещаются, речь не идет о иерархии куч, а о мелких кучах, которые могут иметь любые разрешаемые указатели. Отклоняются несколько концепций, т.к. они не рассматриваются уникальными из-за ограниченности в корректности и не являются сопоставимыми простым образом, дру- гими концепциями: рекурсивные спецификации и полиморфизм в классовых методах. Предикаты высшего порядка разрежаются в принципе, но не рассматриваются отдельно при определении куч (см. четвертую главу). Четвертая глава посвящается доказательству через логическое программирование. Правила Хорна определены так:      T ::= x X [] [ T | Ts ] символ x ∈ X из множества допустимых символов символьная переменная X ∈ X пустой список список с T ∈ X голова терм списка, Ts список остаток     [T , ... , T ] списоксT терм,0 0). Если t ∈ T, то t имеет вид loc → val, иначе t ∈ NT означает, предикат под именем t, который имеется в Γ.
При этом, порядок определения предиката остается в силе. Показано, как кучи ве- рифицируются с помощью распознавателей, чьи формальные грамматики представле- ны правилами Хорна. Абстракция предикатов эквивалентна, при этом параметризацией куч, что эквивалентно атрибутированию данной грамматики.
Преобразование от определения кучи в атрибутированную грамматику можно произ- вести с помощью денотационной функции C и D следующим образом:
C(a) a(⃗y) : −q(⃗xk,n)k×n σ = D qk,n σ(⃗xk,n) ◦ · · · ◦ D qk,1 σ(⃗xk,1).
где C имеет тип atom → predicate → σ → σ, где D имеет тип subgoal → σ → σ, где σ термовая среда имеет тип term∗ → term. Преобразование обратно производится
−1 аналогично с помощью C . .
Связанность, годность и семантические условия куч проверяются для каждего аб- страктного предиката на этапе построения и интерпретации формальной грамматики. Во время распознавания входное слово проверяется со сравниваемой кучей.
Пролог принципиально был предложен, как язык программирования для работы с пре- дикатным представлением. Однако Уоррен, Колвальский и Колмерауер предупреждали, что любые формулы априори не всегда могут быть выводимы. Выводимость зависит от
представления логической формулы и постановления запроса. Для этого имеется два подхода: либо ограничение, либо переоформление правил вывода.
Предикаты высших порядков допускаются, но только не в качестве определения аб- страктного предиката куч. Для куч, предикаты высших порядков не обязательно нужны, с другой стороны, далее абстракция предикатов ломала бы деление между нетермина- лами и терминалами в соответствующей атрибутированной грамматике.
Развертывание/Свертывание (Р/С) предиката a(α⃗) из/в некоторый предикат a для данных предикатов Γa с настоящими значениями термов α⃗/подцелей qk определяется как: a(⃗y) : −qk, где qk = qk,0(⃗xk,0), qk,1(⃗xk,1), …, qk,m(⃗xk,m).
Если α⃗ = (α0, α1, .., αA) и ⃗y = (y0, y1, .., yA), то a(α⃗ ) ⇔ qk,0(⃗xk,0), qk,1(⃗xk,1), …, qk,m(⃗xk,m) с α0 ≈ y0,α1 ≈ y1,…,αA ≈ yA.
Важно заметить, что контекст-свободность распространяется на не повторение одина- ковых терминалов, а на терминалы без атрибутов. Атрибутированные терминалы есте- ственно должны различаться. Транслирующие правила соответствуют подцелям, чьи имена не конфликтуют с остальными предикатами.
Проблема распознавания слова теперь можно сформулировать как α1 , α2 ∈ L(G(P )), где α1,α2 являются входными словами (одно из которых, цепочка терминалов и нетер- миналов, т.е. является спецификацией). L(G(P)) является генерируемым языком грам- матики, который описывается Прологовскими правилами.
Вопрос решаемости о сходимости верификации редуцируем следующим образом: Ес- ли имеются цепочка вывода и правила, то верификация всегда сходима, когда правила детерминированы.
Распознавание слова можно определить с помощью двух операторов вычисления мно- жества наследственных терминалов σ(α) и множества началов нетерминалов π(α). Та- ким образом, доказательство редуцируется на синтаксический перебор.
Проблемы многозначности разрешаются на этапе определений правил абстрактных предикатов куч и на этапе синтаксического перебора. Обсуждаются свойства преобразо- ваний, процесса синтаксического перебора и концепция «Доказательство это синтак- сический анализ», а также границы такого подхода и реализации.
3 Основные выводы и результаты
Основными результатами работы являются следующие:
1 Выполнен анализ существующих ограничений выразимости и для их устранения
предложен унифицированный диалект языка Пролог, позволяющий выполнять одновременную спецификацию и верификацию динамической памяти и, за счёт повышения выразимости, устраняющий многозначность описаний;
2 Разработана обобщенная архитектура верификатора динамической памяти, устраняющая дублирование определений, обеспечивающая расширяемость и ва- риабельность промежуточного представления (IR). Предложена программная реализация верификатора в виде конвейера;
3 В качестве наиболее эффективной для описания абстрактных предикатов куч предложено использование реляционной модели. Продемонстрирована теорети- ческая сводимость предложенного диалекта языка к реляционной алгебре;
4 Обоснована возможность построения новых теорий над кучами до запуска аб- страктных предикатов. Данные теории могут задаваться непосредственно как абстрактные предикаты в диалекте, либо передаваться произвольно задаваемы- ми SAT-решателями в мультипарадигменных средах программирования.
5 Предложены и обоснованы расширения языка моделирования «UML» и языка «OCL» указателями, термами и кучами, показана возможность автоматизиро- ванного вывода над абтрактными предикатами; показаны ограничения представ- ления куч и правил верификации с использованием термов.
6 Показано, что представляемые в диалекте абстрактные предикаты над кучами определяют атрибутную грамматику и то, что синтаксический анализ структуры куч совпадает с процессом их верификации, что определяет возможность авто- матического сравнения динамической памяти с имеющимся экземпляром памяти при условии изменения входных данных
7 Предложено новое графовое определение единичной кучи с помощью конъюнк- ции куч и групповых свойств. Достигнуто упрощение спецификации и верифика- ции с целью ужесточения выражений пространственности куч. Предложен новый способ частичной спецификации объектных экземпляров по виду вычисления Абади-Карделли, которая уменьшает риск не полностью определенных правил.

Актуальность

Ошибки использования динамической памяти являются одними из самых дорогостоящих при разра-
ботке программного обеспечения на протяжении уже нескольких десятилетий. Локализация таких
ошибок является трудной задачей, поскольку, довольно часто, видимое проявление некорректно-
го поведения программы и реальный участок исходного кода его вызвавшего отстоят далеко друг
от друга. Следовательно, разработка подходов и методов, упрощающих поиск и предотвращение
ситуаций некорректного использования динамической памяти является актуальной задачей.
Выразимость утверждений, полнота правил, и автоматизация в большой степени определяют
успех верификации динамической памяти. Выразимость утверждений касается формализма утвер-
ждений и правил верификации. В существующей на текущий момент практике, описания динами-
ческой памяти сложны и часто неинтуитивны. Возможности логического вывода зачастую ограни-
чиваются корректностью и полнотой правил верификации и представляют собой лишь «остров-
ные реализации», которые нельзя использовать на практике. Из-за большого количества соглаше-
ний(конвенций) в языках спецификации и верификации возможности верификации динамической
памяти сильно ограничены.
Верификация часто осуществляется нетривиально, объяснения принятия или отказа доказатель-
ства, как правило, контр-интуитивны.
Диссертационная работа опирается на фундаметальные и прикладные исследования таких ученых
как: Floyd R.W., Hoare C.A.R., Burstall R.M., Kowalski R.A., Clarke E.M. Jr., Apt K.R., Suzuki N.,
Warren D.H.D., Horwitz S., Miller B.P., Fredriksen, L. So, B., Steinbach J., Tofte M., Talpin J.-P., Abadi
M., Hutton G., Reynolds J.C., Berdine J., Calcagno C., O’Hearn P.W. Clarke E.M. Jr., Parkinson M.J.,
Burstall R.M., Hurlin C., Distefano D., Birkedal L., Matthews C., Bertot Y., Gregoire B., Leroy X.,
Dodds M., Jacobs B., Smans J., Philippaerts P., Vogels F., Penninck W., Piessens F. Bornat R., Meyer
B., Parduhn S., Wilhelm R. Leino K.R.M.

Цель работы

Повышение степени выразимости средств описания вариантов использования динамической памяти
за счёт исключения многозначности между языками спецификации и верификации, а также разра-
4

ботка программных средств автоматической верификации.
Работа была осуществлена при поддержке программы №2.136.2014/K от министерства образова-
ния и науки Российской Федерации.

Задачи исследования

Для достижения поставленной цели в диссертационной работе решаются следующие задачи:

1. Исследование и анализ существующих ограничений выразимости и выявление причин несоот-
ветствия языков спецификации и верификации динамической памяти.

2. Исследование декларативности в утверждениях, которые основываются на предикатной ло-
гике без избыточных конвенций и анализ реляционной модели, основанной на ужесточении
пространственных операторов и абстрактных предикатов, для описания куч (от англ. Heap 1 ).
Сравнение реляционной модели предикатов с другими моделями.

3. Исследование критериев реализуемости верификации динамической памяти на основе выбран-
ного логического языка программирования (использующего абстрактную машину Уоррена) и
автоматизированного вывода над абстрактными предикатами. Исследование возможностей и
ограничений при представлении куч, а также правил верификации с помощью термов.

4. Разработка архитектуры верификатора динамической памяти и его программная реализация.

5. Исследование представления куч в таком унифицированном виде, который даёт возможность
обнаружить синтаксически различные, но семантически одинаковые представления и свести
число необходимых сравнений к минимуму. Исследование возможности отделения выраже-
ний куч от остальных логических правил и возможность подключения «SAT »-решателей для
решения отдельных теорий.

6. Исследование возможности автоматического сравнения динамической памяти с имеющимся
экземпляром памяти при условии изменения входных условий или представления модели па-
мяти.

Методы исследования

Автоматизированное доказательство теорем, вычисление Хора, формальная логика, вычислимые
логики, семантики программ, теория типов, теория объектов, логическое программирование, функ-
циональное программирование, объектно-ориентированное программирование, формальные языки,
В работе используется русское название структуры данных „куча“, предложенной Дж. Вильямсом (J. W. J.
Williams) в 1964

Р. Хаберланд
теория языков программирования, теория программирования, теория графов, λ-вычисления, аб-
страктная алгебра, теория вычислимости, языковые процессоры, теория компиляции, логика рас-
пределенной памяти, архитектуры процессоров ЭВМ, организация памяти процессов ОС, встроен-
ные системы, современные технологии моделирования, представление и обработка знаний.

Научная новизна работы

В области автоматизации доказательств:

1. Впервые исследован разрыв между языками спецификации и верификации динамической па-
мяти. Впервые предложен логический язык программирования как инструмент, который спо-
собен преодолеть все выявленные проблемы выразимости, автоматизации и полноты с помо-
щью унификации языков.

2. Впервые проведены сравнения выразимости при трансформации термов в логическом и функ-
циональном представлениях, выявлено с помощью множества примеров при использовании
метрик, что логический язык практически без исключений общности превосходит представ-
ления функционалов. Альтернативно к функционалам рассматривались императивные про-
граммные операторы с побочными эффектами. Оба случаи встречаются в имеющихся подхо-
дах от Reynolds, Parkinson, Berdine, Hurlin, Jacobs, Tofte, Hutton и Bertot, они приводили к
разрыву языков спецификации и верификации.

3. Впервые предложено, термы диалекта языка Пролог использовать непосредственно для пред-
ставления данных полного конвейера статического анализа динамической памяти, в отличие
от используемого в настоящее время комбинированного под- хода Meyer, Leroy, либо подхода
основанного на 3-адресном представление от Reynolds/Berdine, O’Hearn, Bornat, либо подходы
основаны на ассемблере как у Parkinson.

4. Предложен новый метод автоматизации процесса верификации памяти, как синтаксического
перебора абстрактных предикатов, при использовании генеричных интерпретаторов основан-
ных на пошаговой обработке граней графа кучи, в отличие от (полу-)ручного преобразования
структур куч как у Berdine, O’Hearn, а также в отличие от введения определений узкого круга
тактик верификации Bertot и Jacobs.

В области выразимости языков спецификации и верификации:

1. Сняты ограничения выразимости переменных символов, термов и рекурсивных предикатов,
удовлетворяющих правилам Хора для спецификации и верификации динамической памяти, в
отличие от Reynolds, Berdine, Bornat и Parkinson/Hurlin. Ограничения связаны, например, с
использованием как императивной переменной вместо логического символома, а также всвязи

Р. Хаберланд
с логическим представлением правил и его выводом как доказательством теоремы над ди-
намической памятью. Кроме того, сняты ограничения вывода встроенных предикатов, таким
образом, могут произвольно анализироваться определённые абстрактные предикаты во время
запуска программы.

2. Повышена выразимость утверждений в отношении структуры куч за счёт ужесточения опе-
раций над кучами, использовавшиеся ранее и имеющие неоднозначные трактовки в процессе
доказательства, в отличие например от Reynolds, Jones/Hosking, Cormen/Leiserson, Atallah,
Khedker, Muchnik и Pavlu.

Впервые установлены свойства моноида и группы, позволяющие производить вычисления над
кучами одним проходом и без анализа потенциально всех под-выражений динамической па-
мяти, в отличие от Suzuki, Leino и Berdine, а также в отличие от Abadi и Cardelli, которые не
вводят указателей и чьи вычисления строятся на мало интуитивных алгебраических кольцах
с недостатком неполноты и проблемой локальности. Предложено расширить «UML/OCL» с
указателями с ужесточённой моделью.

3. Достигнуто повышение выразимости куч и полноты правил, за счёт введения частичного опе-
ратора «_», которое заменяет переменную или любую часть терма кучи, в отличие от интер-
претируемых предикатов «f alse» и «true» от Reynolds, Berdine/O“Hearn, а также в отличие
от предложенных изменений входного языка Clarke, Apt и Tofte/Talpin.

Теоретическая значимость работы

1. Разработана обобщенная архитектура верификатора динамической памяти на основе конвей-
ера, которая может быть использована и подключена в существующие анализы на основе
Пролог-термов как центральное промежуточное представление.

2. Верификация динамической памяти на основе логического языка программирования является
более адекватным представлением.

3. Абстрактные предикаты могут распознаваться автоматически, т.е. с помощью обобщенного
подхода и без применения тактик.

4. Предложено определение единичной кучи для сокращения многозначности. Предложено вы-
числение для лучшего сравнения куч, а также для улучшения качества программы на более
ранней стадии для возможного включения в моделирования с UML.

5. Сводимость языков верификации и спецификации динамической памяти.

Р. Хаберланд
Практическая значимость работы

При автоматизированной поддержке вывода с повышенной выразимостью теоретически обоснован-
ный и разработанный прототип на основе диалекта Пролога позволяет проводить верификацию
проще и короче.
С практической точки зрения, добавление новых языковых возможностей языка программирова-
ния приводит к новым проблемам между спецификацией и верификацией куч. таким образом: (1)
необходимо проводить спецификации исключительно на логическом/декларативном языке без по-
бочных эффектов, например близком к Прологу; (2) любое представление на языке спецификации
должно обрабатываться элементами языка верификации, какова бы ни была система логического
вывода; (3) языки спецификации и верификации имеют сильные пересечения, и поэтому унифика-
ция обоих языков упрощает оба процесса.
Разработанные в рамках диссертации решения (платформа для верификации, далее – Платформа)
разрешают добавлять новые фазы по обработке динамической памяти, менять существующие и
переводить данные Си-программы в термовое представление. В качестве входного языка может быть
использован любой другой язык, в том числе формально пустой язык. К термовому представлению,
которое также может меняться, могут добавляться новые элементы. Платформа, предложенная на
основе термового представления является открытой.
Теории о кучах можно добавлять произвольно, в том случае если они позволяют синтаксический
перебор. Теории не о кучах также могут быть включены в SAT-решатели.
Предложенное ужесточение куч позволяет решить проблему полноты на основе «неполного опре-
деления синтаксиса», сравнивать кучи и сокращать их описания. Правила состоят из троек Хора,
которые определяют кучи. Если упростить сравнение соседних куч таким образом, что анализиру-
ются только переходные кучи, то правила в общем случае упрощаются. Проверка спецификации
также даёт возможность сравнивать входную и минимальную программы за счёт выявленного гра-
фа кучи. Если автоматизированное доказательство данной теоремы о куче осуществить не удаётся,
то унификация термов Пролога автоматически выявит максимально обобщенный контр-пример без
дополнительных затрат. Ужесточение позволяет последовательно анализировать подкучи и соот-
ветствующие подформулы без возврата и нового поиска. Отпадает анализ всех конъюнкций. Если
данный набор абстрактных предикатов перебирается распознавателям LL(k) или LR(k) и т. д., то
имеется (положительное или отрицательное) доказательство. Практическим компромиссом счита-
ется переоформление правил, которое допускается ради универсальности подхода.
Разработанный диалект Пролога позволяет повысить вызразимость увтерждений куч, автомати-
зировать абстрактные предикаты и упростить спецификацию куч, что в конечном итоге повысит
эффектиность использования разработанного программного средства при решении практических
задач.

Р. Хаберланд
Степень достоверности результатов

Достоверности результатов обеспечивается логическими, формальными выводами и доказательства-
ми представленных в диссертационной работе теорем, а также выполненной реализацией прототипа.
Качество предложенных решений, в том числе универсальных, подтверждается проведённой тща-
тельной экспертизой сравнимости термов на более чем 80 специально подобранных примеров из
большого числа типичных заданий.
Кроме использованных формальных методов, корректность логического вывода основывается на
семантическом анализе, который исключает возможность недопустимых синтаксических и семан-
тических ошибок при предложенной в работе архитектуре конвейера.
Достоверность основных результатов, полученных в диссертационной работе, подтверждается
также их апробацией на различных международных и российских конференциях.

Реализация результатов работы

На основе полученных в диссертационной работе теоретических результатов реализованы прототи-
пы на Прологе с мультипарадигмальным расширением, позволяющие проводить верификацию на
основе синтаксического анализа. Для анализа и сравнения существующих подходов реализованы
ПО «shrinker » для локализации ошибок и ПО «builder » вместо ПО «make».
Результаты диссертационной работы использованы при разработке учебно-методических материа-
лов по λ-вычислениям и введению в систему верификации Coq «Верификация систем программного
обеспечения» на кафедре МО ЭВМ СПбГЭТУ.

Положения выносимые на защиту

1. Диалект языка Пролог, как инструмент для спецификации и верификации динамической па-
мяти.

2. Метод верификации абстрактных предикатов куч на основе распознавания атрибутной транс-
лирующей грамматики.

3. Подход к устранению многозначности описания куч для упрощения их анализа и верификации.

4. Комплекс программных средств для верификации, динамической памяти (Builder, Shrinker,
ProLogika).

Р. Хаберланд
Апробация работы

Основные результаты работы докладывались научных конференциях докладывались и обсуждались
на следующих конференциях:

1. International Conference on Advanced Engineering Computing and Applications in Sciences (ADV-
COMP), (Venice, Italy, 2016)

2. 18th Conference of Open Innovations (FRUCT), (Saint-Petersburg, Russia, 2016)

3. EM C 2 «Технологии Майкрософт в Теории и на Практике Программирования: Новые подходы
к разработке программного обеспечения», (Saint-Petersburg, Russia, 2014)

4. Dynamically Allocated Memory Veriﬁcation in Object-Oriented Programs using Prolog (SYRCoSE),
(Saint-Petersburg, Russia, 2014)

5. Advances in Methods of Information and Communication Technology, (Helsinki, Finland/Petroza-
vodsk, Russia, 2008)

6. A Stricter Heap Separating Points-To Logic, (Moscow, Russia, 2016)

7. International Conference on Control Processes and Stability, (Saint-Petersburg, Russia, 2008)

8. Санкт-Петербургский Электротехнический Университет «ЛЭТИ» (ППС ЛЭТИ), (Saint-Peters-
burg, 2015)

Структура и объем диссертации

Диссертационная работа состоит из введения, пятери глав, заключения, библиографического списка
и приложений. Основная часть работы изложена на 267 страницах и содержит 97 рисунков.
Для введения в предметную область диссертации «Логический язык программирования как ин-
струмент спецификации и верификации динамической памяти» приводится этот раздел. Первый
раздел посвящается вычислению Хора, основным определениям и постановлению решения вычис-
лением, альтернативным подходам и свойствам систем вычислений Хора.
Далее для сравнения различных динамических и статических подходов, можно использовать «ка-
чественную лестницу» из рисунка 1.1 в любой момент. Эта лестница является моим личным пред-
ложением для классификации качества, которое должно соблюдать любое программное обеспече-
ние. Чем больше программа соблюдает критерии качества, тем искреннее можно считать данную
программу качественной. То есть, если программа некорректно вычисляет результат, то на самом
деле можно считать неважным, насколько данная функция выполняет критерий входного домена,
и тем более безразлично, насколько быстро это сделано. Самое главное – это корректное вычисление
программы. Если это соблюдается, то только тогда можно считать уровень «базисно надёжным».

Р. Хаберланд
1. Корректность базисно надёжно
2. Полнота полностью надёжно
3. Оптимальность ресурсов оптимально надёжно

Рисунок 1.1: Качественная лестница по критериям важности

С растущим спросом в надежности растет спрос на универсальность данной функции, т.е. тогда
имеет смысл распространить качество на любые входные функции. Если базисные операции рабо-
тают правильно, то тогда можно требовать, что для всех входных данных функций всё работает
правильно — это второе требование, которое мы обозначим «полностью надёжным», более жёст-
ким, чем первое. Если первые два критерия соблюдаются, то с вычислительной точки зрения, данная
функция корректна и полна. Тогда имеет смысл, далее вводить оптимизации, которые мы обозна-
чим «оптимально надёжными» и которые не меняют вычислительные свойства корректности и
полноты. Надёжными оптимизациями могут послужить, например, ускорение часто востребован-
ных программных блоков, визуализация эффектов, работа с файлами и т.д. Визуальные эффекты
и работа с файлами не будут рассматриваться.
Каждый из установленных критериев можно чётко обозначить и можно предложить некую мет-
рику для измерения выполнимости. Не имеет смысла рассуждать о качестве программы, когда
программа вычисляет корректно и быстро, но не полностью, потому, что универсальность приме-
нения подрывает качество существенно, когда не имеется определение для входного вектора, даже,
если все остальные случаи высчитываются очень быстро. Тогда можно, либо ограничить диапазон
видимости входного вектора для полного покрытия функции, либо сузить покрытие ради неполной
надёжной функции. Когда будут рассматриваться различные подходы, качественная лестница будет
использована как ориентир для принятия или отклонения предложений в дальнейшем.
В данной работе рассматриваются императивные и искусственно-гипотетические языки програм-
мирования. Для практической применимости необходимо рассматривать объектно-ориентирован-
ные модели, поэтому в следующем разделе вводятся основные понятия объектно-ориентированных
вычислений, в частности, Теория Объектов (ТО). Далее рассматриваются теоретические и практи-
ческие проблемы работы с динамической памятью, а затем вводятся модели представления дина-
мической памяти, как, например, анализ образов (АО), вычисление регионов (ВР), а также другие
модели представляющие косвенно-динамическую память. Логика распределённой памяти (ЛРП)
является основной теоретической моделью представления динамической памяти этой работы. За-
тем даётся обзор по автоматизации доказательств и обсуждаются её факторы противостояния. С
целью лучшего понимания проводимых далее доказательств с помощью модели Хора и улучшения
сходимости деревьев доказательств, вводятся представления «абстракции». С кратким обзором по
тематике можно также ознакомиться в [303]. Затем, с целью ознакомления, рассматриваются обла-

Р. Хаберланд
сти применения и связанные с главным направлением работы в этой области, в частности — анализ
псевдонимов (см. раздел 1.4.1), сбор мусора и верификация кода с интроспекцией. В конце этой
главы представляются существующие программные системы и среды.

Р. Хаберланд

Заказать новую

Лучшие эксперты сервиса ждут твоего задания

от 5 000 ₽

Не подошла эта работа?

Закажи новую работу, сделанную по твоим требованиям

Читать

Помогаем с подготовкой сопроводительных документов

Совместно разработаем индивидуальный план и выберем тему работы Подробнее

Помощь в подготовке к кандидатскому экзамену и допуске к нему Подробнее

Поможем в написании научных статей для публикации в журналах ВАК Подробнее

Структурируем работу и напишем автореферат Подробнее

Хочешь уникальную работу?

Больше 3 000 экспертов уже готовы начать работу над твоим проектом!

руководитель успешно защищенных диссертаций, автор около 150 работ, в активе - оппонирование, рецензирование, написание и подготовка диссертационных работ; интересы - ... Читать все

руководитель успешно защищенных диссертаций, автор около 150 работ, в активе - оппонирование, рецензирование, написание и подготовка диссертационных работ; интересы - медицина, биология, антропология, биогидродинамика

#Кандидатские #Магистерские

12 Выполненных работ

Журналист. Младший научный сотрудник в институте РАН. Репетитор по английскому языку (стаж 6 лет). Также знаю французский. Сейчас занимаюсь написанием диссертации по и... Читать все

Журналист. Младший научный сотрудник в институте РАН. Репетитор по английскому языку (стаж 6 лет). Также знаю французский. Сейчас занимаюсь написанием диссертации по истории. Увлекаюсь литературой и темой космоса.

#Кандидатские #Магистерские

11 Выполненных работ

Специальность "Государственное и муниципальное управление" Кандидатскую диссертацию защитил в 2006 г. Дополнительное образование: Оценка стоимости (бизнеса) и госфин... Читать все

Специальность "Государственное и муниципальное управление" Кандидатскую диссертацию защитил в 2006 г. Дополнительное образование: Оценка стоимости (бизнеса) и госфинансы (Казначейство). Работаю в финансовой сфере более 10 лет. Банки,риски

#Кандидатские #Магистерские

123 Выполненных работы

Высшее юридическое образование, красный диплом. Более 5 лет стажа работы в суде общей юрисдикции, большой стаж в написании студенческих работ. Специализируюсь на напис... Читать все

Высшее юридическое образование, красный диплом. Более 5 лет стажа работы в суде общей юрисдикции, большой стаж в написании студенческих работ. Специализируюсь на написании курсовых и дипломных работ, а также диссертационных исследований.

#Кандидатские #Магистерские

158 Выполненных работ

Практикую гражданское, семейное право. Преподаю указанные дисциплины в ВУЗе. Выполняла работы на заказ в течение двух лет. Обучалась в аспирантуре, подготовила диссерт... Читать все

Практикую гражданское, семейное право. Преподаю указанные дисциплины в ВУЗе. Выполняла работы на заказ в течение двух лет. Обучалась в аспирантуре, подготовила диссертационное исследование, которое сейчас находится на рассмотрении в совете.

#Кандидатские #Магистерские

18 Выполненных работ

Более 5 лет помогаю в написании работ от простых учебных заданий и магистерских диссертаций до реальных бизнес-планов и проектов для открытия своего дела. Имею два об... Читать все

Более 5 лет помогаю в написании работ от простых учебных заданий и магистерских диссертаций до реальных бизнес-планов и проектов для открытия своего дела. Имею два образования: экономист-менеджер и маркетолог. Буду рада помочь и Вам.

#Кандидатские #Магистерские

55 Выполненных работ

После окончания института работала экономистом в системе государственных финансов. С 1988 года на преподавательской работе. Защитила кандидатскую диссертацию. Преподав... Читать все

После окончания института работала экономистом в системе государственных финансов. С 1988 года на преподавательской работе. Защитила кандидатскую диссертацию. Преподавала учебные дисциплины: Бюджетная система Украины, Статистика.

#Кандидатские #Магистерские

300 Выполненных работ

Здравствуйте) Имею сертификат специалиста (врач-лечебник). На данный момент являюсь ординатором(терапия, кардио), одновременно работаю диагностом. Занимаюсь диссертац... Читать все

#Кандидатские #Магистерские

13 Выполненных работ

Занимаюсь написанием студенческих работ (дипломные работы, маг. диссертации). Участник международных конференций (экономика/менеджмент/юриспруденция). Постоянно публик... Читать все

#Кандидатские #Магистерские

1386 Выполненных работ