это домашнее задание, но я просто не могу уложить в голове всю эту ерунду с написанием формальных доказательств. Может ли кто-нибудь взломать это и написать формальное доказательство для постусловия этой fnc: строка REPLACE_BY (строка s,char...

Рассмотрим следующий алгоритм min, который принимает списки x, y в качестве параметров и возвращает z-й наименьший элемент в объединении x и y. Предварительные условия: X и Y — отсортированные списки целых чисел в порядке возрастания, и они не...

Я думал о том, что мы можем доказать, что в программе есть ошибки. Мы можем протестировать его, чтобы оценить, насколько он устойчив к ошибкам. Но есть ли способ (даже теоретически) доказать, что в программе нет ошибок? Для простых программ,...

Я пытаюсь узнать об алгоритме Беллмана-Форда, но я застрял с доказательством правильности. Я использовал Википедию , но просто не могу понять доказательство . Я не нашел ничего полезного на Youtube. Надеюсь, кто-нибудь из вас сможет объяснить это...

Функция рекурсивно находит и возвращает наименьший элемент массива, состоящего из целых элементов. Min(A, b, e) if (b=e) return A[b] m = (b+e)/2 // floor is taken x = Min(A, b, m) y = Min(A, m +1, e) If(x < y) return x else...

Это алгоритм: // Precondition: n > 0 l = -1; r = n; while (l+1 != r) { m = (l+r)/2; // I && m == (l+r)/2 if (a[m] <= x) { l = m; } else { r = m; } } // Postcondition: -1 <= l < n Я...

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

Вероятно, это очень простое решение, и я просто тупой, но я не могу найти инвариант для этого цикла while. Для доказательства (a+b) ‹= 2x можно взять (x+y>a+b), поэтому, вероятно, это первая часть инварианта, но для второй части, чтобы доказать 2x‹=...

У меня есть следующий код ATS: extern prfun mul_nx0_0 {n:int} (): MUL(n, 0, 0) extern prfun mul_nx1_n {n:int} (): MUL(n, 1, n) extern prfun mul_neg_1 {m,n,p:int} (MUL(m, n, p)): MUL(~m, n, ~p) extern prfun mul_neg_2 {m,n,p:int} (MUL(m, n, p)):...

В Разработка на основе типов с Idris , говорит Брейди. Если бы вы могли предоставить значение пустого типа, вы могли бы создать значение любого типа. Другими словами, если у вас есть доказательство того, что произошло невозможное значение, вы...