Преподавание программирования и формальных методов

Question

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

Основные нотации: от Discipline of Programming от Dijkstra, а также некоторые параллельные и коммуникационные расширения.

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

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

Answer 1

Чарли,

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

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

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

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

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

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

(Edit:. Вот ссылка на Greg Nelson бумаги, или один из них - CRM)

Answer 2

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

веселит

Answer 3

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

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

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

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

Answer 4

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

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

Answer 5

Игнорируя очевидное то, что ваши favoriteprogramminglanguage ответов, я могу видеть два полезных ответов:

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

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

Answer 6

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

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

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

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

Answer 7

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