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

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

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

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

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

источник

2009-05-07 Charlie Martin

Звучит как действительно интересная книга! – Uri

Спасибо, я буду размещать главы для комментариев, вероятно, связанных с chasrmartin.com. Когда у меня есть главы. –

«Все лучшее» для вашей книги Марти, я просто искал и нашел смысл «формальных методов». – Alphaneo

Чарли,

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

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

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

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

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

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

источник

2009-05-07 03:35:40

Ну, на самом деле я немного поработал с формальным программированием на C; научил его в нескольких мастерских НАСА, NSA, затем меня отвели в компьютерную безопасность. Я помню вещи Грега, теперь, когда ты упоминаешь об этом, мне придется оглянуться на него.Ваша точка зрения о программах do-od EWD и функционале является хорошей; Я бы окончательно определил конструкцию цикла в терминах рекурсии хвоста, если бы пошел так. Я также подумал о том, чтобы объединить их, рассматривая wp как морфизм по векторам состояния, но это может означать, что мне нужно ложиться спать. –

Спасибо за вашу мысль. –

Согласен, вы можете многое сделать с C, но вы сказали, что хотите избежать указателя tarpit. Вообще, когда я задумываюсь о морфизмах, я лежу, пока он не уйдет ... –

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

веселит

источник

2009-05-07 01:03:35 Arnkrishn

Да. Я очень заинтересован в том, чтобы проверить модель на некоторые из этих материалов, но я думаю, что это будет вторая книга. Я пытаюсь подтолкнуть мысль о том, что вы можете научиться думать и, тем самым, программировать, не требуя проверки. –

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

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

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

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

источник

2009-05-07 01:08:52

Я просто ждал звонков на этом :) –

Ну, я проголосовал за вас, это вполне разумный аргумент. Я подозреваю, что люди будут кричать от «формальных методов» задолго до того, как «схема» поймает их внимание. Я немного предвзято отношусь к Win .. Win ... этой другой операционной системе, но там очень много. –

Вы можете легко заменить C# на Java, если это тот тип проблемы. :) Я не уверен, что формальные методы никого не отпугнут ... конечно, не я. Он хорошо выглядит на книжной полке, даже если вы никогда не читали его и не получали от него осмоса. –

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

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

источник

2009-05-07 01:46:29 Svante

Я действительно разорвал это. Im довольно удобно в любом из вариантов, которые я наметил, так что это не проблема, и черт возьми, после 40 лет на этом все они выглядят одинаково в любом случае. Ваша точка зрения о C/Java в порядке, но тогда я делаю это в два этапа: сначала EWD-код, а затем переведите на целевой язык. –

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

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

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

источник

2009-05-07 02:12:51 SingleNegationElimination

Да, это был аргумент EWD. Я не уверен, что я его покупаю - я думаю, что использование реального языка держит вас честными. Я также думал о том, чтобы придумать Ruby DSL в качестве педагогического языка. –

Вы можете использовать настоящий язык или множество реальных языков, каждый из которых тщательно выбирается в каждом случае для максимальной иллюстративной мощности. – SingleNegationElimination

Идите вперед с идеей EWD и используйте свой собственный четко определенный язык. Все реальные исполняемые языки имеют недостатки дизайна и краевые случаи, которые делают их болью. Лучше иметь обозначение/язык, на котором вы можете пройти, и быть уверенным в его исполнении. –

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

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

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

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

источник

2009-06-15 16:51:23

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

источник

2011-02-10 01:01:55 dc42

Хорошо, это выглядит увлекательно. Мне нужно будет изучить это больше, но я ценю указатель. –

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

ответ

Смежные вопросы