Я столкнулся с проблемой, связанной с пост-условием и частичной правильностью этого фрагмента кода. { m = A ≥ 0 } x:=0; odd:=1; sum:=1; while sum<=m do x:=x+1; odd:=odd+2; sum:=sum+odd end while { Postcondition } Я не ищу ответа,...

Я прочитал несколько статей, включая главу Джона Бентли о бинарном поиске. Это то, что я понимаю о ПРАВИЛЬНОЙ логике бинарного поиска, и она работает в простых тестах, которые я сделал: binarysearch (arr, low, high, k) 1. while (low <...

Я читал об инвариантах циклов, но немного запутался. Допустим, у меня есть этот код, каким должен быть инвариант? Что-то вроде А+В=Х? public static void main(String[] args) { Scanner scanner = new Scanner(System.in); long A =...

Учитывая инвариант цикла, Википедия перечисляет хороший способ создать самые слабые предварительные условия для цикла (из http://en.wikipedia.org/wiki/Predicate_transformer_semantics ): wp(while E inv I do S, R) = I \wedge \forall y. ((E...

У меня есть массив "line", в котором содержится строка длины "l", и массив "nl", в котором содержится строка длины "p". Примечание: «l» и «p» не обязательно должны быть длиной каждого соответствующего массива. Параметр «at» будет позицией, в которой...

У меня есть функция sum , которая принимает два массива a и b в качестве входных данных и изменяет b таким образом, чтобы b[i] = a[0] + a[1] + ... + a[i] . Я написал эту функцию и хочу проверить ее с Дафни. Однако Дафни говорит мне, что мой...

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

Это простая задача разделения 0 и 1 в массиве. Я не могу понять, почему инвариант цикла не выполняется. method rearrange(arr: array<int>, N: int) returns (front: int) requires N == arr.Length requires forall i :: 0 <= i <...

Я пытаюсь решить Расстановку монет на LeetCode.com: Всего у вас есть n монет, которые вы хотите сформировать в виде лестницы, где в каждом k-м ряду должно быть ровно k монет. По заданному n найдите общее количество полных рядов лестницы,...

Я пытаюсь решить типичный вопрос бинарного поиска на LeetCode.com : Имея отсортированный (в порядке возрастания) целочисленный массив nums из n элементов и целевое значение, напишите функцию для поиска цели в nums. Если цель существует, вернуть...