OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Среда, 13 Декабрь, 2017 14:06

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 18 ] 
Автор Сообщение
СообщениеДобавлено: Четверг, 09 Январь, 2014 15:35 

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 09 Январь, 2014 17:50 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 8902
Откуда: Россия, Орёл
Из известных на русском Вы, в основном, перечислили всю классику.
У А. П. Ершова есть ряд работ, но они более высоко-научного, чем методического уровня.

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

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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 10 Январь, 2014 09:57 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 620
Откуда: Казань
В книгах Кушниренко очень мало информации по доказательному программированию. В основном дается только определение инварианта.

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 10 Январь, 2014 11:09 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 620
Откуда: Казань
Нашел еще список книг на английском языке:
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.

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 15 Январь, 2014 12:43 

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 15 Январь, 2014 16:15 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 8902
Откуда: Россия, Орёл
Этой нет, но вот вспомнил ещё:
http://gen.lib.rus.ec/book/index.php?md ... 460&open=0


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 21 Февраль, 2014 19:05 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 189
Rifat писал(а):
Какие есть книги по доказательному программированию, желательно, чтобы там была не только сухая теория...

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Воскресенье, 13 Апрель, 2014 13:41 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 620
Откуда: Казань
Заинтересовался следующими книгами:
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)

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Воскресенье, 13 Апрель, 2014 13:53 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 620
Откуда: Казань
Нашел те книги, которые искал в архиве Дейкстры:
http://www.cs.utexas.edu/users/EWD/copyrightsDetail.html
Правда там не печатный текст, а отсканированный рукописный, но читать можно.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 10 Июль, 2014 11:30 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 620
Откуда: Казань
Нашел еще интересную книгу по доказательному программированию:
"The Craft of Programming" John C.Reynolds 1981.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 30 Октябрь, 2014 01:22 

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 30 Октябрь, 2014 16:08 

Зарегистрирован: Пятница, 20 Июль, 2007 17:26
Сообщения: 657
Откуда: Псков
видел англ. оригинал на либрусеке


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Понедельник, 05 Июнь, 2017 23:08 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 620
Откуда: Казань
Rifat писал(а):
Apt, Krzysztof R.; Olderog, Ernst-Rüdiger; Verification of Sequential and Concurrent Programs, Springer-Verlag, New York, 1991.

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

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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Понедельник, 05 Июнь, 2017 23:25 

Зарегистрирован: Понедельник, 30 Июль, 2007 10:53
Сообщения: 1526
Откуда: Беларусь, Минск
Девяносто первый год... В конце девяностых началась разработка JMM - Java Memory Model. В 2004-м она была реализована в JVM. Лет через 7-8 после этого её один раз подправили, и, насколько мне известно, с тех пор она не менялась. Эта же модель памяти используется и в современном C++.

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 06 Июнь, 2017 00:16 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 620
Откуда: Казань
По поводу года издания книги, я читал третье издание от 2009 года. Но там практически весь материал, который не изменяется с годами (если не изменяются законы математики). И книга Discipline of Programming 1976 года сейчас также актуальна.

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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 21 Июль, 2017 17:50 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 620
Откуда: Казань
Кто-нибудь знает, где можно скачать книгу?
Programming with Specifications
An Introduction to ANNA, A Language for Specifying Ada Programs
David Luckham


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Суббота, 22 Июль, 2017 00:34 

Зарегистрирован: Воскресенье, 03 Февраль, 2008 12:50
Сообщения: 226
Rifat, на http://gen.lib.rus.ec/ есть.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Воскресенье, 23 Июль, 2017 21:32 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 620
Откуда: Казань
Большое спасибо!


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 18 ] 

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 2


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2005-2017, участники конференции «OberonCore», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Без разрешения участников и ссылки на конференцию «OberonCore» любое воспроизведение и/или копирование высказываний полностью и/или по частям запрещено.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB