Что доказывает, что две сложные программы эквивалентны?

Question

Допустим, я хотел доказать, что две программы эквивалентны (либо строго если это возможно, или неофициально если нет).Более конкретно, скажем, у меня есть что-то относительно сложное, такое как HTTP-сервер, реализованный на C, и один, реализованный в Node.js / JavaScript.Что я могу сделать, чтобы сказать: "эти два фактически одно и то же"?Какие у меня есть варианты?Что возможно?Что невозможно?

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

По сути (я воображаю) Я хочу сказать "эти две программы на JS и C делают одно и то же".Это "сделайте то же самое" очевидно, что это расплывчато, но в то же время это означает что-то конкретное.Любой наблюдаемый результат в любой системе, как правило, одинаков, плюс - минус.Так что это похоже на доказательство, но не являясь Идеальный доказательство.Как будто это частичное доказательство или что-то в этом роде.

Я хотел бы иметь возможность сказать о своих программах: "эти две реализации эквивалентны по всем статьям".Вероятно, я бы начал с предоставления измеримых гарантий или наблюдений за производительностью и поведением ввода-вывода, а затем написал бы несколько тестов, и ...Я не совсем помню, как-то делал заявления об этой системе.Или я должен просто думать, что "функционирующий HTTP-сервер на любом языке является АКСИОМА".Это упростило бы его :) Просто предположим, что он делает то же самое, что и каждый другой.Но мне кажется, что это уклонение от темы.

Интересно, какие у меня здесь есть варианты?Как далеко я могу зайти в этом теоретически?Меня не волнует, сколько времени потребуется для реализации или определения этого, если на это уйдут годы, прекрасно.Я просто хотел бы знать, что возможно с точки зрения того, чтобы сделать утверждение "эти две программы на C и JS эквивалентны" более строгим и обоснованным.Какие методы / теории / направления исследований я мог бы изучить, чтобы сделать это возможным?

Прямо сейчас я просто предполагая они неявно равны, что позволяет моему коду вызывать либо функцию C, либо функцию JS, зная, что ~ общий эффект ~ один и тот же (я знаю, туманно, не знаю, как это определить).Я хотел бы применить к этому некоторую математику, проверку модели, программную симуляцию или что-то в этом роде, чтобы я мог сделать его более надежным, если это возможно :)

На другом конце спектра находится доказательство того, что 3 > 2 эквивалентен как в C, так и в JS.Что я вообще должен делать в этом простом случае?Делая это немного более сложным на пути к полноценному HTTP-серверу, копирование строки в C сильно отличается от копирования в JavaScript, но это относительно простая вещь.Где мне вообще начать доказывать, что эти "операции" эквивалентны между двумя языками?Или если не "доказать", то просто "заявить", что они эквивалентны, с какими-то запасными доказательствами или что-то в этом роде, я не знаю.

Здесь это немного, но эта диаграмма - это то, что я в основном пытаюсь сделать:

На более широком уровне проблема, по-видимому, аналогична этой....Допустим, я хочу получить медальон.Я могу либо пойти в магазин и купить его, либо напечатать в 3D.Оба "алгоритма" (поход в магазин или 3D-печать) сильно отличаются друг от друга, но фактически они одинаковы.Не было бы простого способа поэтапно доказать, что они эквивалентны оперативно (исходя из того, что дает мое воображение), но очевидно, что конечный результат тот же.Как бы вы (даже здесь) сформулировали это со всей строгостью?

Answer 1

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

В вашем случае код любой из двух программ явно слишком сложен для полного формального анализа:

• Проверка модели работать не будет.
• Полное (bi-) моделирование также не будет работать.

Итак, лучшее практическое решение, которое я знаю, это тестирование на основе модели.Хотя это и не является доказательством, все же можно использовать формальные методы.Это в конечном счете устраняет проблему написания и сопровождения тестовых примеров, написанных вручную.

P.S.:

Краткий список шагов, которые можно выполнить в этом случае:

• Создается абстрактная модель двух программ.Это третья реализация, в которой будут опущены все несущественные детали.Преимущество абстракции в том, что эта модель снова достаточно проста для формального анализа.Модель может быть реализована на любом языке, который вам нравится, если анализатор модели проанализирует байтовый код.
• Абстрактная модель может быть пройдена, и, например,покрытие условия достигается в наборе тестов.Этот шаг выполняется с помощью инструмента тестирования на основе модели.
• Наконец, эти тестовые примеры тестируются на двух программах и проверяется, может ли абстрактная модель имитировать две реализации программы.
• Это имитационное соотношение, конечно, не является доказательством эквивалентности.
• Абстракция - это очень чистая спецификация того, что было учтено в наших тестах и что было опущено.
• Два инструмента тестирования на основе моделей, которые могут быть рекомендованы:Microsoft Spec Explorer, Разработчик Conformiq

Answer 2

Один может написать целую методику съемки книги о доказательной программной эквивалентности. Этот ответ так же как очень короткая отправная точка:

Теоретически, если вы думаете о ваших программах в качестве Turgining Machines, то вся надежда потеряна - доказывая, что два TMS имеют одинаковый язык (т. Е. Они семантически эквивалент) неразрешен (на самом деле , это не в Re $ \ cup $ Core).

Все еще теоретически, если вы думаете о ваших программах как конечных станков, включая состояния памяти как часть машины, то эквивалентная программа для DFAS очень проста (разрешима в NL), а для NFAS это полное Pspace Отказ Проблема с таким подходом состоит в том, что пространство состояния будет огромным (например, если у вас есть только 100 битов памяти, ваше пространство штата имеет по крайней мере $ 2 ^ {100} $ Штаты), так что это неразумно.

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

в основном, это поле Формальная проверка и именно некоторые ключевые слова, которые могут получить Вы начали:

.
• Проверка модели
• Бисимуляция
• абстракция - Уточнение
• Теорема Проверены (например, CoQ)

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