В общем, вы не можете сделать это из-за проблемы с остановкой. Вы даже не можете решить, остановится ли функция («return»).
Как практический вопрос, есть немного больше надежды. Если вы ищете пузырьковой сортировки, вы можете решить, что он имеет ряд частей:
- а к-быть отсортирован типа данных S с частичным порядком,
- контейнерный тип данных C с одной переменной экземпляра а («массив»)
- , что удерживает чтобы быть отсортированные данные
- ключ типа к («индекс массива») используется для доступа к контейнеру, который имеет частичный порядок таким образом, что контейнер [к] тип S
- сравнение двух элементов контейнера, используя ключ A и ключ B такой, что A < B в соответствии с ключевым частичным порядком, который определяет , если контейнер [B]> контейнер A
- операция подкачки на контейнере [A], контейнер [B] и некоторая переменная T типа S, то есть conditionaly зависит от сравнения
- цикл обернуты вокруг контейнера, в котором перечислены ключи в соответствии частичный порядок на K
Вы можете создать кусочки кода, которые находят каждый из этих битов данных в исходном коде, и если вы найдете их всех, утверждают, что у вас есть доказательства пузыря.
Чтобы сделать это конкретно, необходимо стандартный анализ программы машины:
- для синтаксического анализа исходного кода и создания абстрактного синтаксического дерева
- символ сборки таблицы (ST), что знать тип каждого идентификатора где используется
- построить граф потока управления (CFG), чтобы вы проверили, что различные распознанные биты встречаются в соответствующем порядке
- построить граф потока данных (DFG), чтобы вы могли определить, какие значения распознаны в одной части поток алгоритма правильно в другой части
[Это много машин просто начать работу]
Здесь вы можете написать специальный код процедурного кода, чтобы подняться над AST, ST, CFG, DFG, чтобы " признать "каждую из отдельных частей. Это, вероятно, будет довольно грязным, поскольку каждый распознаватель будет проверять эти структуры для подтверждения своего бита. Но ты можешь сделать это.
Это довольно грязный и достаточно интересный материал, поэтому есть инструменты, которые могут многое сделать.
Наш набор инструментов для реинжиниринга программного обеспечения DMS является одним из них. DMS уже содержит все механизмы для стандартного анализа программ для нескольких языков. DMS также имеет язык соответствия шаблону потока данных, вдохновленный Rich and Water's 1980's "Programmer's Apprentice" ideas.
С DMS, вы можете выразить эту конкретную проблему примерно так (непроверенная):
dataflow pattern domain C;
dataflow pattern swap(in out v1:S, in out v2:S, T:S):statements =
" \T = \v1;
\v1 = \v2;
\v2 = \T;";
dataflow pattern conditional_swap(in out v1:S, in out v2:S,T:S):statements=
" if (\v1 > \v2)
\swap(\v1,\v2,\T);"
dataflow pattern container_access(inout container C, in key: K):expression
= " \container.body[\K] ";
dataflow pattern size(in container:C, out: integer):expression
= " \container . size "
dataflow pattern bubble_sort(in out container:C, k1: K, k2: K):function
" \k1 = \smallestK\(\);
while (\k1<\size\(container\)) {
\k2 = \next\(k1);
while (\k2 <= \size\(container\) {
\conditionalswap\(\container_access\(\container\,\k1\),
\container_access\(\container\,\k2\) \)
}
}
";
В каждом шаблоне, вы можете написать, что сводится к конкретному синтаксису выбранного языка программирования («домен шаблона»), ссылаясь на потоки данных, названные в строке подписи шаблона. Подшаблон можно упомянуть внутри другого; необходимо передать потоки данных в и из подшаблона, назвав их. В отличие от «простого старого C», вы должны передать контейнер явно, а не путем неявной ссылки; это потому, что нас интересуют фактические значения, которые текут из одного места в шаблон в другой. (Просто потому, что два места в коде используют одну и ту же переменную, не означает, что они видят одно и то же значение).
Учитывая эти определения и попросить «сопоставить bubble_sort», DMS посетит DFG (привязан к CFG/AST/ST), чтобы попытаться сопоставить шаблон; где он совпадает, он привяжет переменные шаблона к записям DFG. Если он не может найти соответствия для всего, матч терпит неудачу.
Для достижения соответствия каждый из приведенных выше шаблонов преобразуется по существу в свой собственный DFG, а затем каждый шаблон сопоставляется с DFG для кода, используя так называемый тест изоморфизма подграфа. Построение DFG для patter принимает лот машин: синтаксический анализ, разрешение имен, управление и анализ потока данных, применяемые к фрагментам кода на языке оригинала, смешанные с различными мета-экранами. Изоморфизм подграфов является «простым» для кодирования, но может быть очень дорогостоящим для запуска. Что экономит шаблоны шаблонов DMS, так это то, что большинство шаблонов имеют множество ограничений [tech point: и у них нет узлов), и каждый попытка совпадения имеет тенденцию терпеть неудачу довольно быстро или полностью преуспевает.
Не указано, но, определяя различные биты отдельно, можно обеспечить альтернативные реализации, позволяющие распознавать варианты.
Мы использовали это, чтобы реализовать полностью готовые инструменты для извлечения заводских контрольных образцов от реальных промышленных контроллеров завода для Dow Chemical на их специфическом языке Dowtran (это означало, что для парнеров и т. Д., Как указано выше для Dowtran). У нас есть версия этого прототипирования для C; анализ потока данных сложнее.