статический анализ — Строгое доказательство свойства следующего кода C ++?

Question

статический анализ — Строгое доказательство свойства следующего кода C ++?

Возьмите следующий фрагмент кода C ++ 14:

unsigned int f(unsigned int a, unsigned int b){
if(a>b)return a;
return b;
}

Утверждение: функция f возвращает максимум своих аргументов.

Теперь утверждение «очевидно» верно, но я не смог доказать это строго в отношении ISO / IEC 14882: 2014 (E) Спецификация.

Первый: Я не могу заявить собственность формально.

Формализованная версия может быть:
За каждое утверждение s, когда абстрактная машина (которая определена в спецификации) находится в состоянии п а также s выглядит как «F (expr_a,expr_b) «и ‘f’ в s разрешается к рассматриваемой функции, s (P) .return = max (expr_a (P). Return, expr_b (P). Return).

Здесь для государства п и выражение s, S (P) это состояние машины после оценки s.

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

Редактировать: Может быть оформлено в Coq

8

c++coq proof-of-correctness static-analysis

Решение

Другие решения

Мне кажется, что самое простое решение — доказать это задом наперед. Если первый аргумент f является максимальным аргументом, докажите, что возвращается первый аргумент (довольно просто — максимальный аргумент a по определению больше b). Если второй аргумент является максимальным аргументом, докажите, что второй аргумент возвращается. Если они равны, покажите, что уникального элемента максимума нет, поэтому второй аргумент все еще максимальный аргумент.

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

2

Я не уверен, что вы хотите. Глядя на предыдущую версию N3337, мы можем легко увидеть, что указано почти все:

a и b начинаются с вызывающих значений (функция 5.2.2 — 4)
Вызов функции выполняет составной оператор тела функции (очевидно, но где?)
Заявления обычно выполняются по порядку (Заявления 6)
If-операторы выполняют первый под-оператор if, если условие истинно (If-оператор 6.4.1)
Отношения действительно работают, как и ожидалось (операторы отношений 5.9 — 5)
Оператор возврата возвращает значение вызывающей функции (Оператор возврата 6.6.3)

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

1

Источник

Accepted Answer

Пожалуйста, извинитесь за мои приблизительные знания математики старения.

Максимум для замкнутого подмножества натурального числа (BN) можно определить следующим образом:

Max:(BN,BN) -> BN
(x ∊ BN)(a ∊ BN)(b ∊ BN)(x = Max(a,b)) => ( x=a & a>b | x=b )

где символ имеет общее математическое значение.

Хотя ваша функция может быть переписана следующим образом, где ООН является ансамблем unsigned int:

f:(UN,UN) -> UN
(x ∊ UN)(a ∊ UN)(b ∊ UN)(x = f(a,b)) => ( x=a && a>b || x=b )

Где символ = operator==(unsigned int,unsigned int), так далее…

Таким образом, вопрос сводится к тому, чтобы узнать, определяет ли стандарт, что математическая структура (и), образованная unsigned integer с C ++ арифметическими операторами и оператором сравнения изоморфный к математическим структурам (классам, категориям), образованным замкнутым подмножеством N с общей арифметической операцией и отношениями. Я думаю, что ответ — да, это выражается простым английским языком:

Стандарт C ++ 14,[Expr.rel] / 5 (Реляционные операторы)

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

Стандарт C ++ 14, [Basic.fundamental] / 4 (Основные типы)

Целые числа без знака должны подчиняться законам арифметики по модулю 2n, где n — число битов в представлении значения этого конкретного размера целого числа.

Тогда вы могли бы также доказать это ({true,false},&&,||) также изоморфна булевой арифметике, анализируя текст в [Expr.log.and]
а также [Expr.log.or]

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

4