final-report-andrianov-2010 (1184401)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Московский государственный университет имени М. В. ЛомоносоваФакультет вычислительной математики и кибернетикиОтчет по практикумуЖадный алгоритм для задачи о выборе заявокИсполнитель:студент 528 группыАндрианов Иван АлексеевичПреподаватель:доктор физ.-мат. наукПетренко Александр КонстантиновичМосква, 2010СодержаниеПостановка задачи...............................................................................................................3Тестирование алгоритма.....................................................................................................4Описание спецификации целевой функции..................................................................4Обоснование выбранных ветвей функциональности ..................................................4Характеристики покрытия исходного кода реализации ...............................................4Сравнение выбранных ветвей функциональности и ветвей покрытия по исходномукоду ...................................................................................................................................5Описание принципов выбора тестовых данных и их количественных характеристик...........................................................................................................................................5Оценки минимальности набора тестовых данных с точки зрения покрытия ветвейфункциональности и исходного кода ............................................................................5Описание ошибок в реализации, которые были выявлены при помощитестирования ...................................................................................................................5Верификация алгоритма......................................................................................................6Описание спецификации требований в синтаксисе ACSL ..........................................6Описание ошибок в реализации, которые были выявлены при помощиверификации ...................................................................................................................6Описание выбранных инвариантов и вариантов .........................................................6Количество и классификация сгенерированных лемм ................................................7Выводы, сделанные по результатам верификации .....................................................7Заключение...........................................................................................................................82Постановка задачиПусть даны n заявок на проведение занятий в одной и той же аудитории.

Дваразных занятия не могут перекрываться по времени. В каждой заявке указаныначало и конец занятия (si и fi для i-й заявки). Разные заявки могут пересекаться повремени, тогда можно удовлетворить только одну из них. Каждая заявка отождествляется с промежутком [si, fi), так что конец одного занятия может совпадать сначалом другого, и это не считается пересечением. Заявки с номерами i и j называются совместными, если интервалы [si, fi) и [sj, fj) не пересекаются (иными словами,если fi ≤ sj или fj ≤ si). Задача о выборе заявок состоит в том, чтобы набратьмаксимальное количество совместных друг с другом заявок.Жадный алгоритм работает следующим образом. Предполагается, что заявкиупорядочены в порядке неубывания времени окончания: f1 ≤ f2 ≤ ...

≤ fn. По ходуработы алгоритма составляется множество номеров выбранных заявок. В начале вэто множество добавляется первая заявка. Далее на каждом шаге во множестводобавляется первая заявка, не пересекающаяся с последней добавленной. Реализация алгоритма на языке С представлена в тексте 1. Здесь s и f — массивы начал иконцов заявок, n — количество заявок, result — результирующий массив номеровзаявок, а возвращаемое значение — количество заявок, включенных врезультирующий массив.unsigned gas(double * s, double * f, unsigned n, unsigned * result){unsigned i, j, k;result[0] = 0;k = 1;j = 0;for(i = 1; i < n; i++){if(s[i] >= f[j]){result[k] = i;k++;j = i;}}return k;}Текст 1.

Реализация жадного алгоритма для задачи о выборе заявокТребуется протестировать указанный алгоритм с помощью инструментаCTesK, а затем верифицировать алгоритм с помощью инструментов Frama-C, AltErgo, PVS.3Тестирование алгоритмаОписание спецификации целевой функцииПредусловия:•n строго больше 0.•s содержит по меньшей мере n элементов.•f содержит по меньшей мере n элементов.•result содержит по меньшей мере n элементов.•Элементы f упорядочены по неубыванию.•Элементы s строго меньше элементов f с теми же индексами.Постусловия:•Элементы result упорядочены по возрастанию.•Элементы result больше или равны 0 и строго меньше n.•Заявки с номерами, включенными в result, не пересекаются.•Для каждой заявки, номер которой не включен в result, найдется заявка с номером, включенным в result, которая с ней пересекается.Обоснование выбранных ветвей функциональностиВетви функциональности:1.

На входе имеется одна заявка.2. На входе имеются непересекающиеся заявки.3. На входе имеются заявки, часть из которых пересекается, а часть нет.4. На входе имеются заявки, каждая из которых пересекается хотя бы с однойдругой заявкой.Данные ветви функциональности соответствуют различным вариантам поведения функции. В первом случае в результирующем массиве должен быть номерединственной заявки.

Во втором случае в результирующем массиве должны бытьномера всех заявок. В третьем случае в результирующем массиве должны бытьномера заявок, которые не пересекаются с другими, и часть номеров остальныхзаявок. В четвертом случае в результирующем массиве должна быть часть номеровзаявок.Характеристики покрытия исходного кода реализацииПокрытие исходного кода во время тестирования составляет:•100% строк исходного кода•100% ветвей исходного кода4Сравнение выбранных ветвей функциональности и ветвей покрытия поисходному кодуВ связи с тем, что было достигнуто полное покрытие ветвей исходного кода, аветви функциональности соответствуют различным вариантами поведения функции,то каждой ветви покрытия соответствует некая ветвь функциональности.Описание принципов выбора тестовых данных и их количественныххарактеристикТестовые данные для первой ветви функциональности, а именно 2 вещественных числа, были заданы вручную.

Тестовые данные для остальных ветвей выбирались с помощью линейных функций. В цикле из 10 итераций вычислялись значениялинейных функций в точке, равной номеру итерации.Оценки минимальности набора тестовых данных с точки зренияпокрытия ветвей функциональности и исходного кодаНабор тестовых данных, скорее всего, минимальным не является, однако онбыл выбран в силу простоты алгоритма его порождения.Описание ошибок в реализации, которые были выявлены при помощитестированияПри тестировании ошибок в реализации выявлено не было.5Верификация алгоритмаОписание спецификации требований в синтаксисе ACSLrequires n > 0;requires \valid_range(s, 0, n - 1);requires \valid_range(f, 0, n - 1);requires \valid_range(result, 0, n - 1);requires \forall unsigned i, j; 0 <= i <= j < n ==> f[i] <= f[j];requires \forall unsigned i; 0 <= i < n ==> s[i] < f[i];ensures \forall unsigned i; 1 <= i < \result ==> result[i - 1] < result[i];ensures \forall unsigned i; 0 <= i < \result ==> 0 <= result[i] < n;ensures \forall unsigned i; 1 <= i < \result ==> f[result[i - 1]] <= s[result[i]];ensures \forall unsigned i; 0 <= i < n && (\forall unsigned j; 0 <= j < \result ==> result[j] != i) ==> (\existsunsigned k; 0 <= k < n && (\exists unsigned l; 0 <= l < \result && result[l] == k) && (s[k] < f[i] <= f[k] || s[i] <f[k] <= f[i]));Данная спецификация эквивалентна спецификации, описанной в предыдущейглаве.Описание ошибок в реализации, которые были выявлены при помощиверификацииПри верификации ошибок в реализации выявлено не было.Описание выбранных инвариантов и вариантовloop invariant 1 <= i <= n;loop invariant 0 <= j < i;loop invariant 1 <= k <= i;loop invariant result[k - 1] == j;loop invariant result[k - 1] == i - 1 || s[i - 1] < f[j];loop invariant \forall unsigned l; 1 <= l < k ==> result[l - 1] < result[l];loop invariant \forall unsigned l; 0 <= l < k ==> 0 <= result[l] < n;loop invariant \forall unsigned l; 1 <= l < k ==> f[result[l - 1]] <= s[result[l]];loop invariant \forall unsigned m; 0 <= m < i && (\forall unsigned l; 0 <= l <k ==> result[l] != m) ==> (\exists unsigned o; 0 <= o < i && (\existsunsigned p; 0 <= p < k && result[p] == o) && (s[o] < f[m] <= f[o] || s[m] <f[o] <= f[m]));loop variant n - i;•Первый инвариант означает, что по ходу выполнения цикла i всегда большеили равен 1 и меньше или равен n.•Второй инвариант означает, что по ходу выполнения цикла j всегда больше6или равен 0 и строго меньше i.•Третий инвариант означает, что по ходу выполнения цикла k всегда большеили равен 1 и меньше или равен i.•Четвертый инвариант означает, что j представляет собой последний номер,добавленный в result, а k — количество номеров заявок, добавленных в result.•Пятый инвариант означает, что либо номер i - 1 был включен в result, либозаявка с таким номером пересекается с заявкой с номером j.•Шестой инвариант означает, что по ходу выполнения цикла элементы resultвсегда упорядочены по возрастанию.•Седьмой инвариант означает, что по ходу выполнения цикла элементы resultвсегда больше или равны 0 и строго меньше n.•Восьмой инвариант означает, что по ходу выполнения цикла заявки с номерами, включенными в result, всегда не пересекаются.•Девятый инвариант означает, что по ходу выполнения цикла каждая рассмотренная заявка, номер которой не включен в result, пересекается с некоторойрассмотренной заявкой, номер которой включен в result.•Вариантом является разность n - i, так как n постоянен, i меньше или равно n,и i увеличивается на 1 после каждой итерации цикла.Количество и классификация сгенерированных лемм•Всего: 62•Условия верификации: 44•Условия завершимости: 18Выводы, сделанные по результатам верификацииНикаких допущений, обеспечивающих корректность алгоритма, при верификации сделано не было.

Никаких проблем с инструментами верификации не возникло.7Заключение•Количество строк кода реализации: 20•Количество строк спецификации в нотации ACSL: 21•Количество тестов: 4•Количество доказанных лемм: 59 автоматически, 3 с помощью PVS•Время затраченное на разработку тестов: 5 часов•Время затраченное на доказательство корректности: 120 часовПоставленная задача решена полностью. Функция gas протестирована с помощью инструмента CTesK, а затем верифицирована с помощью инструментов FramaC, Alt-Ergo, PVS.По результатам работы можно сделать вывод, что верификация даже достаточно простой функции с помощью инструментов может занимать длительное время.Ручное доказательство лемм для данной функции заняло бы на порядок меньшевремени.8.

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов учебной работы