Обучение программированию и формальным методам

Question

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

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

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

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

Answer 1

Чарли,

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

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

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

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

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

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

(Редактировать:Вот ссылка на Грег Нельсон бумага или один из них.— CRM)

Answer 2

Игнорирование очевидного, что является вашим любимым < a href = "https://stackoverflow.com/questions/273108/which-programming-languages-have-helped-you-to-understand-programming-better"> программирование language ответы, я вижу два полезных ответа:

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

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

Answer 3

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

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

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

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

Answer 4

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

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

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

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

Answer 5

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

ваше здоровье

Answer 6

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

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

Answer 7

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