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

Ответ 1

Чарли,

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

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

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

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

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

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

(Edit: Здесь ссылка на документ Грега Нельсона или один из них - CRM)

Ответ 2

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

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

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

Ответ 3

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

С# - очень простой язык для изучения, и он получил все основы, которые вам нужно было бы быстро погрузиться в такие темы, как concurrency. Он имеет большую применимость, так как вы можете ориентироваться на OO и веб-концепции. Он также довольно популярен, и вы получите компании, оплачивающие книги своих сотрудников, которые всегда хороши для продаж ( "Be a Kick Ass С# Programmer" идет гораздо дальше на лист возмещения расходов, чем "Concurrency в Modern Lisp" ).

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

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

Ответ 4

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

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

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

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

Ответ 5

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

веселит

Ответ 6

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

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

Ответ 7

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