final-report-grechanik-2010 (решения 2010 года), страница 2

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

Поэтомубыло принято решение преобразовать функцию таким образом, чтобы все утверждения,касающиеся императивной части реализации, были доказаны автоматически.Рассмотрим общую схему работы функции:void __bitmap_shift_right(unsigned long *dst,const unsigned long *src, int shift, int bits){for (k = 0; k < l(shift, bits); ++k)dst[k] = g(shift, bits, src[m(k)], src[m(k) + 1], k);if (off(shift))memzero(&dst[lim(bits) - off(shift)], off(shift));}Функции l, lim, g, m и off являются функциями в математическом смысле.Можно записать эту функцию и ещё проще (псевдокод):for each (dst[k])dst[k] = f(shift, bits, src, k);Таким образом после выполнения цикла и вызова memzero будет выполнено следующееутверждение:7∀n ∈ N.(0 ≤ n < lim) ⇒ dst[n] = f (shift, bits, src, n)Тогда единственной существенной леммой будет лемма о том, что из этого утверждениеследует постусловие:\forall integer k;0 <= k < n ==> bit_at(a, n, sa + k) == bit_at(b, n, sb + k)Функция была переписана соответствующим образом.

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

Это помогло только частично, поэтому данный путь также был признантупиковым.3.6Неисследованные путиОдним из возможных способов доказательства корректности функции является сведение постусловие к исходной функции при помощи эквивалентных преобразований. В этомслучае постусловие рассматривается как неэффективная, но очевидно корректная реализация.

Главное преимущество этого подхода – возможность конструировать эффективныефункции одновременно с доказательством их корректности.Тем не менее, этот подход может также привести к разрастанию формулы и проявлению тех же проблем, что и раньше.3.7Выводы, сделанные по результатам верификацииАлгоритм является корректным при допущении корректности алгоритма.Основные недостатки инструментов:• Большое количество ошибок в jessie-плагине.• Экспоненциальный взрыв количества сгенерированных лемм при большом количестве выражений типа bool.• Необоснованный мусор в результирующем pvs-файле (например neq_int_bool).8• pvs по всей видимости распараллелен не более, чем на два потока.

Это же в некоторойстепени касается и графического интерфейса jessie-плагина.• Язык ACSL недостаточно интегрирован с языком C.• pvs неудобен.94Заключение• Количество строк кода реализации: 59• Количество строк спецификации в нотации ACSL: 211• Количество тестовых вариантов: 2747• Количество доказанных лемм: 197 автоматически, 1 с помощью PVS частично• Время затраченное на разработку тестов: неизвестно• Время затраченное на доказательство корректности: неизвестноПоставленная изначально задача не решена и не может быть решена с использованиемпредложенных методов решения в установленные сроки, включая время на обучение pvs1 .1Не исключено, что человек, обладающий многолетним опытом использования pvs, сможет относительно легко доказать нужную лемму, потому что будет знать правильный подход к таким задачам (например,что лучше pvs для таких задач не использовать)10.