Обучение программированию и формальным методам - PullRequest
22 голосов
/ 07 мая 2009

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

Основная нотация будет из дисциплины программирования Дейкстры , вместе с некоторыми расширениями для параллелизма и коммуникации.

В отличие от EWD, я хочу, чтобы мои ученики в конечном итоге писали реальные исполняемые программы. Это означает, что в какой-то момент перевод с нотации EWD на другой язык. Когда я впервые начал заниматься формальным программированием, я нацелился на C, но в итоге вы пишете много слесарного дела, плюс есть все сложности обработки указателей и т. Д. Ruby является очевидной возможной целью, как Scheme или Lisp. Но есть также различные функциональные языки; так как я особенно заинтересован в параллелизме, Erlang кажется вероятным.

Итак, наконец, вот мой вопрос: на каком языке (языках) я должен учить своих читателей ориентироваться на их формально разработанные программы?

Ответы [ 7 ]

18 голосов
/ 07 мая 2009

Чарли,

Я всегда связывал шедевр Дейкстры с моделью программирования, в которой центральная сцена занята циклами и массивами. Если вы придерживаетесь Dijkstra (например, вычисляете самые слабые предварительные условия), я думаю, вы найдете функциональные языки не очень подходящими. Из популярных языков, которые обеспечивают хорошую поддержку императивного программирования с помощью циклов и массивов, возможно, Python несет наименьший дополнительный багаж.

Это не означает, что функциональные языки не подходят для формальных методов - они очень хорошо подходят - но стиль довольно отличается от Dijkstra. Предпочтительные методы подчеркивают расчетные доказательства; см. статью Ричарда Берда о решении судоку (что очень тяжело) или учебник Ричарда Берда и Фила Уодлера.

Для параллелизма это во многом зависит от того, в какую модель параллелизма (и в какие формальные методы) вы верите. Concurrent ML Джона Реппи - прекрасная модель передачи сообщений. У Эрланга также есть хорошая чистая ограничительная модель. С другой стороны, программирование с блокировками и критическими секциями настолько сложно, что формальные методы в этой ситуации могут принести больше пользы.

Два других мимолетных замечания, которые могут представлять интерес для вашего базового исследования:

  • Единственным программистом, которого я когда-либо встречал, кто применял методы Дейкстры на практике к реальным системам, был Грег Нельсон, который работал в Модуле-3. (Грег и Марк Манассе вместе написали оконную систему Trestle.) Modula-3 был очень хорошим языком, который Digital позволил умереть от беспомощности и некомпетентности. У Грега была хорошая статья в TOPLAS о расширении исчисления Дейкстры.

  • Язык моделирования Джерарда Хольцмана SPIN основан непосредственно на языке защищенных команд Дейкстры и поддерживает параллелизм. Его целью является проверка моделей, а не программирование, и здесь есть несколько особенностей, но существует тесная связь с формальными методами, и действительно здорово иметь возможность проверять модели своими утверждениями. Любой, кто интересуется формальными методами, захочет проверить это.

(Правка: Вот ссылка на статью Грега Нельсона или одну из них. - CRM)

7 голосов
/ 07 мая 2009

Не обращая внимания на очевидный, какой ваш любимый программирование язык ответов, я вижу два полезных ответа:

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

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

3 голосов
/ 07 мая 2009

Я вырос на Лиспе и Схеме и люблю их обоих. Я думаю, что это отличные языки для изучения с нуля. Но я не уверен, что кто-то с некоторым опытом программирования пойдет на эти языки. Вы не получите много хитов на Amazon для своей книги со Схемой в названии. :)

C # - очень простой в изучении язык, и в нем есть все основы, которые вам понадобятся, чтобы довольно быстро погрузиться в такие темы, как параллелизм. У него больше применимости, потому что вы можете ориентироваться на ОО и веб-концепции. Он также довольно популярен, и вы получите от компаний, которые платят за книги своих сотрудников, которые всегда хороши для продаж («Станьте программистом на языке C #» гораздо дальше, чем «Параллелизм в современном Лиспе»).

F # - интересный язык. Он обладает функциональной красотой Lisp или Scheme (ну, не совсем, но почти), и дает вам некоторую возможность погрузиться в темы ООП, а также подключиться к .NET Framework для пользовательского интерфейса, если вы хотите оживить ситуацию. Но сейчас это неясно.

Я не могу говорить с Руби, так что лично я бы укусил пулю и пошел с C #.

2 голосов
/ 15 июня 2009

Честно говоря, я не могу рекомендовать Руби для этого. Когда я программирую изо дня в день в своем коммерческом мире, мне это очень нравится, гораздо больше, чем C или Java. Но его семантика настолько плохо определена, что я не доверяю ей вдвое меньше, чем C, где, хотя я могу потратить несколько часов на споры по поводу утверждения и консультации с более толстой белой книгой, заменившей K & R, я выхожу в Я уверен, что если у меня есть соответствующий компилятор (да, я знаю, я мечтатель, но работаю со мной здесь), я знаю, что получится с другой стороны.

Ruby прекрасен во многих отношениях, но что касается формального, он никогда не встретится.

Я бы склонялся голосовать за Хаскелла сам, потому что каждый раз, когда я оборачиваюсь, я поражаюсь, насколько много смысла в этом определении языка. (Хотя, по общему признанию, после года или около того, я уверен, что я не исследовал половину углов даже на Haskell 98.)

И я тоже понимаю, что Дикжстра против функциональности; возвращаясь и читая его бумаги он очень в императивном мире; Я не квалифицирован, чтобы сказать, действительно ли он ошибся там. Возможно, я просто ошеломлен тем, насколько хорошо его письмо, а также его мысли. Но это, похоже, ему понравилось, так что насчет использования Алгола 60 ?

1 голос
/ 10 февраля 2011

Есть довольно много университетов, использующих Perfect Developer для обучения формальным методам (отказ от ответственности: я связан с этим продуктом). Он построен на языке для выражения спецификаций, уточнения данных и алгоритмов. Он имеет автоматическую проверку теорем для проверки и генератор кода, который может производить C ++, C # и Java. Проект PD был очень вдохновлен «Дисциплиной программирования», однако мы обнаружили, что обозначения довольно непрактичны для больших систем, поэтому обозначения несколько отличались от обозначений Дейкстры.

1 голос
/ 07 мая 2009

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

Лично я бы использовал Common Lisp, так как я знаком с этим, и это отличный язык для реализации любой концепции. Другими вариантами могут быть Erlang, Haskell, Ruby или Python, возможно, даже некоторый диалект ML. Я предвзято отношусь к семейству C (включая C # и Java), они, похоже, придерживаются более низкого уровня мышления о концепциях.

1 голос
/ 07 мая 2009

Это хорошая идея. Я думаю, что Схема - хороший вариант, так как позволяет применять на практике (в форме библиотек) различные абстракции с минимальными необходимыми элементами. Также легко перевести схему в систему верификации, такую ​​как PVS (http://pvs.csl.sri.com/)

ура

...