Приемы построения программ - Методичка

МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ Федеральное государственное автономное образовательное учреждение высшего профессионального образования Приемы построения программ для студентов дневного и вечернего отделений факультета математики, механики и компьютерных наук Часть 1" разработаны сотрудником кафедры прикладной математики и программирования старшим преподавателем Невской Е.С.Методические указания содержат примеры построения программ с использованием двух методов: 1) метода построения программы с одновременным доказательством ее правильности, 2) метода сведения к более простым задачам. Методические указания состоят из двух частей. Первая часть методических указаний посвящена первому методу. Вторая часть методических указаний посвящена второму методу. Первый метод требует введения терминологии: понятий спецификации, предусловия, постусловия, инварианта и ограничивающей функции.Прежде чем разрабатывать алгоритм решения задачи, а затем программу, надо понять задачу. В программировании такое описание называется спецификацией программы (задачи). Определить спецификацию - значит прежде всего подобрать точные понятия, адекватные задаче. Главное - определить понятия, используемые в спецификациях. Свойство спецификаций, отличающее их от алгоритмов (и от программ) определяется так: "Спецификация описывает, что надо сделать, а не как это делать".Вводятся: квантор $ (обозначающий "существует"), квантор "(обозначающий "для всех") и квантор N (обозначающий "количество"). Семантика такова: существует по крайней мере одно (целое) i такое, что m ? i ? n, для которого выполнено Ei, то есть принимает значение истина (true). Семантика такова: для всех i из области m ? i ? n Ei принимает значение истина (true). Семантика такова: число различных значений i из области m ? i ? n, при которых Ei принимает значение истина (true). Семантика такова: сумма значений, определенных индексом i из области m ? i ? n, при которых Ei принимает значение истина (true).Обозначение определяет следующий смысл: "Если выполнение S началось в состоянии, удовлетворяющем Q, то имеется гарантия, что оно завершится через конечное время в состоянии, удовлетворяющем R". Программа S называется правильной (по отношению к данным предусловию Q и постусловию R), если имеет место {Q} S {R}. Предикат Q называется предусловием (или входным утверждением) S, предикат R - постусловием (ли выходным утверждением). Конечно, все это верно, если S работает не бесконечно (проблема останова) и (что самое главное) Q правильно формирует начальное состояние данных задачи перед выполнением S, а R правильно формирует конечное состояние данных задачи после выполнения S. Это обстоятельство является главным аргументом противников такого метода построения программ, так как доказательство правильности программы заменяется доказательством правильности спецификаций (Q и R).Наша задача при данных предусловии Q и постусловии R перед определением цикла построить для него инвариант и ограничивающую функцию. Инвариант P строится путем анализа и преобразования постусловия R. Инвариант можно рассматривать как ослабление постусловия R. Таким образом, множество состояний, удовлетворяющих P, должно содержать как множество возможных начальных состояний, так и множество конечных состояний, отраженное в R. В качестве примера рассмотрим задачу линейного поиска значения x в массиве a [1: n] при условии, что x содержится в массиве.Массив из одного элемента считается упорядоченным. Определим постусловие R: значение p будем считать длиной максимальной площадки, если существует в массиве последовательность из p равных значений и нет последовательности из p 1 равных значений. Для этого заменим в R константу n переменной i и добавим границы изменения переменной i, тогда получим инвариант P: (1 ? i ? n) and ($ j: 1 ? j ? i-(p-1): b [j] = b [j p-1]) and (" j: 1 ? j ? i-p: b [j] ? b [j p]), где p - длина максимальной площадки в массиве b [1: i]. Опишем алгоритм в виде процедуры Plosh в следующей интерпретации: заменим два условных оператора в короткой форме одним условным оператором в короткой форме (выносим оператор i: = i 1; из условных операторов). const n_max=20; Для выделения каждой площадки требуется организовать циклический процесс, инвариант которого имеет вид: (" j: i ? j ? n-j: b [j] = b [i]), где i - индекс очередного элемента массива.Найти элемент x в матрице a [1: n,1: m]. Перейдем к построению тела цикла, которое предназначено для уменьшения ограничивающей функции. Тело цикла выполняется при условии В этом случае для перехода к следующему элементу следует начать с новой строки, то есть выполнить операторы: i: = i 1; j: = 1; При построении алгоритма естественно воспользоваться вложенными циклами: внешний цикл по строкам (переменная i) и внутренний цикл по столбцам (переменная j).Текстовый файл представлен в виде последовательности строк. Каждая строка состоит из последовательности целых чисел, разделенных про

Содержание

Введение

1. Основная терминология

1.1 Спецификация программ

1.2 Логические средства

1.3 Предусловие и постусловие

1.5 Способы построения инварианта

2. Примеры построения программ

2.1 Выделение последовательности из массива

2.2 Поиск элемента в матрице

2.3 Поиск элемента в текстовом файле

2.4 Обработка строк

2.5 Работа с массивами

Литература

Методические указания содержат примеры построения программ с использованием двух методов: 1) метода построения программы с одновременным доказательством ее правильности, 2) метода сведения к более простым задачам.

Методические указания состоят из двух частей. Первая часть методических указаний посвящена первому методу. Вторая часть методических указаний посвящена второму методу.

Первый метод требует введения терминологии: понятий спецификации, предусловия, постусловия, инварианта и ограничивающей функции. Эти понятия связаны с построением цикла. Оператор цикла является одной из самых важных конструкций алгоритмического языка. Программ без цикла практически не бывает.

Построение программы начинается с определения спецификации задачи - что дано и что нужно найти. Затем формулируются предусловие и постусловие.

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

Этот метод построения программы относится к методу аналитического вывода программы, что подтверждает ее правильность.

Второй метод (сведение решения задач к решению более простых задач) иллюстрируется на задачах: перестановка сегментов в массиве, "Быстрая сортировка", удаление из последовательности повторяющихся элементов. Эти задачи рассматриваются во второй части методических указаний. программа инвариант массив спецификация