webew
Войти » Регистрация
 
Алгоритмы

Дейкстра о тестировании

28 ноября 2012, 2:20
Автор: rgbeast
В книге "Дисциплина программирования" (1976) Э. Дейкстра пишет "Даже в случае полностью детерминированных машин полезность тестирования программ оказывается сомнительной. Тестирование программы может вполне эффективно служить для демонстрации наличия в ней ошибок, но, к сожалению, непригодно для доказательства их остуствия". Далее Дейкстра развивает подход, в котором операторы языка рассматриваются как преобразователи предикатов, а верность программы можно доказать математически с помощью формальной логики.

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

Есть ли прогресс в рамках математического подхода доказательства корректности программ? Какие-то новые книги, учебные курсы, программные средства?
Добавить комментарий
Отображение комментариев: Древовидное | Плоское

1234ru

Цитата:
Далее Дейкстра развивает подход, в котором операторы языка рассматриваются как преобразователи предикатов, а верность программы можно доказать математически с помощью формальной логики.

Как такой подход выглядит на практике? Нет ли какого-нибудь примера?
То, что не убивает нас, делает нас инвалидами.
29.11.2012, 05:14
Ответить
NO USERPIC

rgbeast

1234ru
Как такой подход выглядит на практике? Нет ли какого-нибудь примера?

Примеры подробно описаны в книге Дейкстры. Идея основана на следующем: у нас есть некоторое начальное состояние, а в результате работы программы получается конечное состояние. Программа связывает логические утверждения о начальном состоянии с логическими утверждениями о конечном состоянии, причем это можно записать языком формальной логики для всех промежуточных состояний. Такой подход позволяет доказать, что на выходе получится правильный ответ (состояние определенного вида) при определенных условиях на начальное состояние. Строгое доказательство исключает ошибки и необходимость тестирования (опять же см. книгу).
29.11.2012, 07:48
Ответить
NO USERPIC

info21

Еще источники с примерами:

Грис. Наука программирования. Мир, 1984

Вирт. Алгоритмы и структуры данных, ДМК Пресс.
Конкретно насчёт цикла Дейкстры -- см. там примеры в главе 1.9.
Примеры к книжке Вирта можно скачать отдельно (http://www.inr.ac.ru/~info21/ADru/)

Инвариант цикла + Цикл Дейкстры + эвристика "идти с конца" -- это главные фишки у Дейкстры.

Как и с математическими доказательствами, в реальности формальные рассуждения в 95% случаев не нужны, в остальных случаях рассуждения полуформальны, хотя в учебниках они прописываются со всеми деталями, чего в реальной жизни не бывает.
Этого многие не понимают и встают на дыбы.

В компьютерном классе с грамотным преподом это освоить нетрудно, если с нуля.
Трудно бывает переучивать свой головной мозг, когда чел с 14 лет привык хвататься за for-break.

В быстрой сортировке цикл разделения сегмента тоже мило переписывается на трехветочный цД.

С цД проблема отладки сложных спутанных циклов исчезает как класс.
Подобные ситуации встречаются не так часто, но когда встречаются, без цД бывает реальная засада.

Первый раз меня Дейкстра спас в 96 году, в заковыристом алгоритме слияния в алгебраической сортировке (где нужно как можно раньше учитывать, что могут складываться и сокращаться подобные). Там еще в цикл была вживлена рекурсия, и мало не показалось.

Последний раз -- шестиветочный цД (эквивалент шести спутанных циклов-пока) корректно заработал с первого раза. (Этот пример -- в софте на указанном сайте Информатики-21, в исходнике модуля i21sys/Mod/Vocabulary.odc -- там реализуется закулисный перевод ключевых слов с русского на английский, чтобы потом можно было вставить маркеры ошибок в правильные точки русского исходника, это нужно для 5-7-классников).

Или вот на днях аспирант после компьютерного класса радостно переписал на двухветочный цД некий нестандартный цикл "односторонней оптимизации", позвольте не вдаваться, но после переписывания полегчало.

Успехов!
30.11.2012, 23:32
Ответить

1234ru

Серьезный текст..
Читая его, я подумал, что программирование для веб (по крайней мере, повседневное) практически не ставит перед разработчиками серьезных алгоритмических задач.
На практике чаще приходится решать проблемы правильности работы программ (что происходит от плохой организации процесса разработки, в частности, отсутствия документации и нехватки времени), чем оптимизировать собственно действия, которые программа выполняет.
Во многом, это происходит по причине использования нескольких технологий, и узкие места часто находятся вне программы как таковой (например, получение ответа от базы данных и пр.; вообще само по себе использование языков высокого уровня уже, видимо, снижает простор для возможных оптимизаций), что кардинально снижает вклад оптимизации алгоритмов в итоговое быстродействие программ. Еще сильнее это усугубляется современными вычислительными мощностями, которые позволяют обеспечить очень быстрое выполнение даже не совсем оптимальных алгоритмов.

Все это, конечно, не повод писать некачественный код.

info21, за ваш комментарий хочу выразить признательность. Судя по всему, при вдумчивом чтении он может немало обогатить знаниями.
То, что не убивает нас, делает нас инвалидами.
04.12.2012, 21:53
Ответить
NO USERPIC

rgbeast

Есть архитекторы, которые строят новые мосты и уникальные здания, а есть те, кто проектирует кварталы панельных домов. Вторая задача более массовая и, на первый взгляд, требует меньше фундаментальных знаний, но цена ошибки высока и на это место предпочтут взять человека, который умеет строить нетиповое. Аналогично в веб-разработке: массы занимаются сборкой из готовых блоков по готовым рецептам, но на конференциях (Highload, РИТ) наибольший интерес вызывают доклады тех, кто собственно веб-разработкой не занимается, а, например, разрабатывает движок базы данных или веб-сервер. Работа последних связана, в основном, с алгоритмами и от них ждут новых идей и новых блоков для сборки программ. Это отражается и на зарплате специалистов по алгоритмам, когда они устраиваются на работу в интернет-компании.

Дествительно, сейчас компьютер является over-qualified для многих задач, для которых он применяется (например, управление кассовым аппаратом или стиральной машиной). Тем не менее, случаи неоправданного пренебрежения алгоритмами не так редки. Все сталкивались с повисшими кассовыми аппаратами или мобильниками, которые медленно откликаются на клавиши. Другой пример - проверка зависимости пакетов при установке или обновлении linux/windows, которая почему-то занимает несколько минут, а не несколько миллисекунд (речь идет всего лишь о тысячах пакетов).
05.12.2012, 08:39
Ответить
© 2008—2017 webew.ru, связаться: x собака webew.ru
Сайт использует Flede и соответствует стандартам WAI-WCAG 1.0 на уровне A.
Rambler's Top100