OberonCore
https://forum.oberoncore.ru/

Книги по доказательному программированию
https://forum.oberoncore.ru/viewtopic.php?f=75&t=4927
Страница 1 из 2

Автор:  Rifat [ Четверг, 09 Январь, 2014 15:35 ]
Заголовок сообщения:  Книги по доказательному программированию

Какие есть книги по доказательному программированию, желательно, чтобы там была не только сухая теория, но и приводились бы примеры реального кода на существующем языке или псевдокоде?
Хотелось бы что-нибудь наподобие книг (можно на русском или английском):
- Дейкстра "Дисциплина программирования"
- Грис "Наука программирования"
- Вирт "Систематическое программирование" (1 глава из этой книги)
- Бейбер "Программное обеспечение без ошибок"
- Baber "The Spine Of Software"

Автор:  Илья Ермаков [ Четверг, 09 Январь, 2014 17:50 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

Из известных на русском Вы, в основном, перечислили всю классику.
У А. П. Ершова есть ряд работ, но они более высоко-научного, чем методического уровня.

Отметить ещё нужно мехматовский учебник Кушниренко "Программирование для математиков".
http://www.niisi.ru/kumir/books.htm
Да и в "Основах И и ВТ" есть элементы доказательного программирования (+ "12 лекций о том, для чего нужен школьный курс математики и как его преподавать").

Также отметим вузовские учебники сибиряков:
Касьянов "Курс программирования на Паскале в задачах и упражнениях" - НГУ.
Костюк "Основы программирования. Разработка и анализ алгоритмов" - ТГУ.

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

Автор:  Rifat [ Пятница, 10 Январь, 2014 09:57 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

В книгах Кушниренко очень мало информации по доказательному программированию. В основном дается только определение инварианта.

Вспомнил еще одну книгу по доказательному программированию:
Андерсон Р. Доказательство правильности программ. М.: Мир, 1982

Автор:  Rifat [ Пятница, 10 Январь, 2014 11:09 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

Нашел еще список книг на английском языке:
Recommended reading
* Abrial, J.-R., The B-Book: Assigning Programs to Meanings, Cambridge University Press, Cambridge, 1996.
Apt, Krzysztof R.; Olderog, Ernst-Rüdiger; Verification of Sequential and Concur¬rent Programs, Springer-Verlag, New York, 1991.
* Baber, Robert L., The Spine of Software: Designing Provably Correct Soft¬ware — Theory and Practice, John Wiley & Sons, Chichester, 1987.
* Baber, Robert L., Error-free Software: Know-How and Know-Why of Program Correctness, John Wiley & Sons, Chichester, 1991.
* Baber, Robert L., Praktische Anwendbarkeit mathematisch rigoroser Methoden zum Sicherstellen der Programmkorrektheit, Walter de Gruyter, Berlin, 1995.
* Baber, Robert L., The Ariane 5 explosion as seen by a software engineer, http://www.cs.wits.ac.za/~bob/ariane5.htm, 1997 February.
* Backhouse, Roland C., Program Construction and Verification, Prentice-Hall International, Englewoods Cliffs, N. J. 1986.
de Bakker, J. W., Mathematical Theory of Program Correctness, Prentice-Hall International, Englewood Cliffs, N. J., 1980.
* Cohen, Edward; Programming in the 1990s: An Introduction to the Calculation of Pro-grams, Springer-Verlag, New York, 1990.
Denvir, Tim, Introduction to Discrete Mathematics for Software Engi¬neer¬ing, Macmillan Education, Basingstoke, 1986.
* Dijkstra, Edsger W., A Discipline of Programming, Prentice-Hall, Inc., En¬glewood Cliffs, N. J., 1976.
* Gries, David, The Science of Programming, Springer-Verlag, New York, Heidelberg, Berlin, 1981.
* Kaldewaij, Anne; Programming: The Derivation of Algorithms, Prentice-Hall In¬ter¬na¬tional, 1990.
Linger, Richard C.; Mills, Harlan D.; Witt, Bernard I., Structured Pro¬gram¬ming: Theory and Practice, Addison-Wesley Publishing Co., Read¬ing, Massachusetts, 1979.
Loeckx, Jacques; Sieber, Kurt, The Foundations of Program Verification, B. G. Teubner, Stuttgart, und John Wiley & Sons, Chichester, 1984.

Кто-нибудь что-нибудь читал из этого (помимо Дейкстры, Гриса и Бейбера) и может порекомендовать?

Автор:  Rifat [ Среда, 15 Январь, 2014 12:43 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

Есть у кого-нибудь книга?
Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ. М.: Радио и связь, 1988.

Автор:  Илья Ермаков [ Среда, 15 Январь, 2014 16:15 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

Этой нет, но вот вспомнил ещё:
http://gen.lib.rus.ec/book/index.php?md ... 460&open=0

Автор:  PSV100 [ Пятница, 21 Февраль, 2014 19:05 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

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

Имхо, чтобы взглянуть как может предельно абстрактный математический аппарат работать и на практике, то и смотреть необходимо кроме классики теории ещё и классику практики -- системы на базе зависимых типов и публикации вокруг них -- Agda (хотя здесь реальная практика под вопросом), Idris, ATS, плюс Coq (правда, фактически, это доказатель теорем, пример его использования -- CompCert, С-компилятор, доказывающий результаты своей работы), системы по-проще -- Liquid Types (основы), ещё проще -- вряд ли применимы, например: Typestate Is Dead.

Автор:  Rifat [ Воскресенье, 13 Апрель, 2014 13:41 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

Заинтересовался следующими книгами:
Predicate Calculus and Program Semantics (Monographs in Computer Science)
by Edsger W. Dijkstra (Author), Carel S. Scholten (Author)
и
Formal Development of Programs and Proofs
by Edsger Dijkstra (Author), E. W. Dijkstra (Author)

Может быть есть у кого-нибудь эти книги или знаете где можно их найти?

Автор:  Rifat [ Воскресенье, 13 Апрель, 2014 13:53 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

Нашел те книги, которые искал в архиве Дейкстры:
http://www.cs.utexas.edu/users/EWD/copyrightsDetail.html
Правда там не печатный текст, а отсканированный рукописный, но читать можно.

Автор:  Rifat [ Четверг, 10 Июль, 2014 11:30 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

Нашел еще интересную книгу по доказательному программированию:
"The Craft of Programming" John C.Reynolds 1981.

Автор:  Rifat [ Четверг, 30 Октябрь, 2014 01:22 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

Кто-нибудь знает где можно найти книгу:
Проектирование корректных структурированных программ / С. Алагич, М. Арбиб ; Пер. с англ. под ред. О. М. Рякина, 264 с. ил. 22 см, М. Радио и связь 1984 ?

Автор:  albobin [ Четверг, 30 Октябрь, 2014 16:08 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

видел англ. оригинал на либрусеке

Автор:  Rifat [ Понедельник, 05 Июнь, 2017 23:08 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

Rifat писал(а):
Apt, Krzysztof R.; Olderog, Ernst-Rüdiger; Verification of Sequential and Concurrent Programs, Springer-Verlag, New York, 1991.

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

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

- необходима практика конструирования программ, использующих недетерминированность, для того, чтобы легче было доказывать распределенные параллельные программы.

Автор:  Valery Solovey [ Понедельник, 05 Июнь, 2017 23:25 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

Девяносто первый год... В конце девяностых началась разработка JMM - Java Memory Model. В 2004-м она была реализована в JVM. Лет через 7-8 после этого её один раз подправили, и, насколько мне известно, с тех пор она не менялась. Эта же модель памяти используется и в современном C++.

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

Автор:  Rifat [ Вторник, 06 Июнь, 2017 00:16 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

По поводу года издания книги, я читал третье издание от 2009 года. Но там практически весь материал, который не изменяется с годами (если не изменяются законы математики). И книга Discipline of Programming 1976 года сейчас также актуальна.

Выводы мои. Первые два следуют из материала книги. Третий - это чисто мой вывод.

По поводу JMM, возможно, она и решает какие-то проблемы. Но я практически уверен, что не гарантирует безошибочность программы. Поэтому к книге это имеет небольшое отношение. Так как книга описывает общий случай.

Автор:  Rifat [ Пятница, 21 Июль, 2017 17:50 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

Кто-нибудь знает, где можно скачать книгу?
Programming with Specifications
An Introduction to ANNA, A Language for Specifying Ada Programs
David Luckham

Автор:  kemiisto [ Суббота, 22 Июль, 2017 00:34 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

Rifat, на http://gen.lib.rus.ec/ есть.

Автор:  Rifat [ Воскресенье, 23 Июль, 2017 21:32 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

Большое спасибо!

Автор:  Rifat [ Суббота, 03 Ноябрь, 2018 23:51 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

Rifat писал(а):
В книгах Кушниренко очень мало информации по доказательному программированию. В основном дается только определение инварианта.

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

Автор:  Валерий Лаптев [ Воскресенье, 04 Ноябрь, 2018 08:52 ]
Заголовок сообщения:  Re: Книги по доказательному программированию

Почему-то никто не назвал книгу http://www.studmed.ru/anderson-r-dokaza ... 03b60.html
Андерсон Р.Д. Доказательство правильности программ.
Там же: Вельдер С.Э. и др. Верификация автоматных программ

Еще порекомендую книжку по Model Checking Карпова
http://avidreaders.ru/book/model-checki ... ennyh.html
Это как раз о верификации параллельных программ

Страница 1 из 2 Часовой пояс: UTC + 3 часа
Powered by phpBB® Forum Software © phpBB Group
https://www.phpbb.com/