работа с аморфными подсистемами в формальном дизайне программного обеспечения

Такие люди, как Александр Степанов и Шон Пэрент, голосуют за формальный и абстрактный подход к проектированию программного обеспечения.
Идея состоит в том, чтобы разбить сложные системы на ориентированный ациклический граф и скрыть циклическое поведение в узлах, представляющих это поведение.
Пэрент проводил презентации. на boost-con и в Google (листы с boost-con , стр. 24 знакомит с подходом, есть также видео выступления Google Talk) .

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

Как бы это решить?
Обратите внимание, что я просто ищу абстрактный подход.

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


architecture software-design generic-programming language-agnostic
person Georg Fritzsche    schedule 20.10.2009    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Ваш вопрос не ясен. Определите аморфные подсистемы.

Вы «просто ищете абстрактный подход», но затем, похоже, вам нужны подробности о реализации на обычном языке программирования («общий шаблон для конечных автоматов»). Итак, что вы просите? Как реализовать вложенные конечные автоматы?

Еще немного подробностей поможет разговору.

Для настоящего абстрактного подхода посмотрите что-то вроде Потоковая передача X-Machines:

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

Stream X-Machine отличается от модели Эйленберга тем, что основной тип данных

X = Выход* × Память × Вход*,

где In* — входная последовательность, Out* — выходная последовательность, а Mem — оставшаяся часть памяти.

Преимущество этой модели в том, что она позволяет управлять системой шаг за шагом через ее состояния и переходы, наблюдая за выходными данными на каждом шаге. Это значения-свидетели, которые гарантируют, что определенные функции выполнялись на каждом шаге. В результате сложные программные системы могут быть разложены на иерархию машин Stream X-Machine, спроектированных сверху вниз и протестированных снизу вверх. Этот подход «разделяй и властвуй» к проектированию и тестированию поддерживается доказательством правильной интеграции Флорентином Ипате, которое доказывает, что независимое тестирование многоуровневых машин эквивалентно тестированию составной системы. ...

Но я не понимаю, как презентация связана с этим. Кажется, он говорит о вполне мейнстримном подходе к программированию, ничего похожего на X-Machines. В любом случае, презентация довольно запутанная, и у меня сейчас нет времени смотреть видео.

Первое впечатление от доклада, чтение только слайдов

Автор бессистемно затрагивает многочисленные области/проблемы/решения, по-видимому, не осознавая этого: из Peopleware ( например, от Психология программирования), до Разработка программного обеспечения (например, программное обеспечение линейки продуктов), до различных методов программирования.

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

Если/когда я увижу видео, я обновлю этот ответ.

person MaD70    schedule 21.10.2009
comment
Спасибо за отзыв, прочитаю после работы. Быстро для общего шаблона: просто быстрый пример, полученный из моего опыта C++. - person Georg Fritzsche; 21.10.2009
comment
Ну, я не думал о независимости от языка - я думаю, этот подход имеет смысл только с языками, в которых у вас есть универсальное программирование. Кроме того, он исходит из C++ и, похоже, сильно зависит от направления, в котором началась STL. Хотя ваши ссылки интересны, они не очень помогают мне с моим вопросом. - person Georg Fritzsche; 24.10.2009
comment
Также я думаю, что такие подходы, как логика Хоара, не популярны по одной причине - я знаю проверенные микроядра, но не что-то подходящего размера. По крайней мере, направление, в котором пошла STL, стало несколько популярным, и это несмотря на то, что нет способа действительно проверить смоделированные концепции во время компиляции. - person Georg Fritzsche; 24.10.2009
comment
Что ж, в первой части я действительно пытался понять ваш вопрос, я пытался сформулировать его с помощью хорошо понятных концепций (так что мой намек на потоковые X-машины FSM). Извините, но я пока не понимаю вашего вопроса. w.r.t. мои комментарии к слайдам: Логика Хоара не лучший вариант, а ПТоП (Практическая Теория Программирования) гораздо проще. Для языков программирования со сложными системами типов трудности различаются. - person MaD70; 24.10.2009
comment
В любом случае это только примеры. Я утверждаю: зачем изобретать совершенно новый словарь, когда существуют предыдущие варианты? Я думаю, что для сравнительной формальной аргументации концепции не кажутся более простыми. - person MaD70; 24.10.2009
comment
Хм, тогда мне придется читать в aPToP. С моим недостающим теоретическим образованием (прикладная информатика) я склонен рассматривать большинство теоретических подходов как излишние и неподходящие для более крупного проекта. Подход из презентации вытекал из формализации практических соображений, что для меня более естественно. Хотя может это просто предубеждение с моей стороны :) - person Georg Fritzsche; 24.10.2009
comment
Я обнаружил, что все усилия по C++ были ошибочными, и эти концепции C++ соответствовали им: упражнение в усложнении. Доказательством этого является, например, наше обсуждение синтаксического анализа C++ — см. комментарий Иры Бакстер (stackoverflow.com/questions/1520734/): правила для этого [построение таблицы символов программы C++] занимает большую часть 600-страничного справочного руководства. С учетом этих предпосылок я могу только представить усилия по анализу и доказательству свойств программы на C++ (это уже сложно для программы на C). - person MaD70; 27.10.2009
comment
Тем не менее, я нашел полезной для мотивации моего интереса к aPToP эту статью Хенера Что не так с формальными методами программирования? (cs.toronto.edu/~hehner/wrong.pdf): он сравнивает три хорошо известных формализма - логику Хоара, семантику преобразования предикатов Дейкстры и Венское развитие Джонса. Метод (ВДМ) - с собственным АПТоП. - person MaD70; 27.10.2009
comment
Кроме того, из предисловия к книге aPToP: Теория в этой книге проще, чем любая из только что упомянутых. [Те же три теории, упомянутые выше] В ней спецификация — это просто логическое выражение. Уточнение — это просто обычное значение. Эта теория также является более общей, чем только что упомянутые, и применяется как к завершающим, так и к незавершающим вычислениям, как к последовательным, так и к параллельным вычислениям, как к автономным, так и к интерактивным вычислениям. - person MaD70; 27.10.2009
comment
Обратите внимание в разделе 4.0.4 Программы на важную концепцию, часто неправильно понимаемую: Программа — это спецификация поведения компьютера; на данный момент это означает, что это логическое выражение, связывающее предсостояние и постсостояние. Не всякая спецификация является программой. Программа — это реализованная спецификация, т. е. спецификация, для которой была предоставлена ​​реализация, так что компьютер может ее выполнить. То есть программа, написанная на языке программирования ( PL) является формальной спецификацией в любом случае. Качество такой ЯП (формальной нотации) имеет решающее значение для формального обоснования такой спецификации. - person MaD70; 27.10.2009
comment
Конечно, одного ЯП недостаточно для выражения всех спецификаций, т. е. даже не реализуемых спецификаций, которые необходимо уточнять в программах. - person MaD70; 27.10.2009
comment
Я обновил свой ответ ссылкой на CSP Хоара, чтобы не создавалось впечатление, что Хоар ничего не производил из 60-х годов. - person MaD70; 27.10.2009
comment
На выходных постараюсь залезть в неверный.pdf/apToP. Я знаю, C++ — это не тот язык, о котором люди любят формально рассуждать в деталях, но опять же, я думаю о гибкости и выразительности, которые он имеет, что позволяет обойти некоторые ограничения, с которыми я только что сталкивался в большинстве других языков, с которыми я рисковал. Хм, но, возможно, языки, которые слишком выразительны, просто не работают, когда они также нацелены на сложные приложения и правильность. - person Georg Fritzsche; 28.10.2009
comment
К сожалению, в настоящее время aPToP не имеет инструментальной поддержки (вам нужно закодировать его законы в средстве доказательства теорем) и не интегрирован с языком программирования. ATS (компиляция в C), Qi (компиляция в Common Lisp) и Epigram (интерпретатор) являются полными решениями. ATS кажется более практичным (если вы не программируете на Лиспе) и в настоящее время разрабатывается. С помощью ATS вы можете перейти от обычной статической типизации (ну, обычной, если вы привыкли к ML или Haskell) к полноценному программированию с доказательством теорем. Производительность близка к C (по крайней мере, в одноядерной версии). Я согласен, что мы еще не совсем там, но... - person MaD70; 28.10.2009
comment
.. мы близки к полезным формальным рассуждениям об инфраструктуре программ. Обратите внимание, что с полностью проверенными библиотеками и формально определенным API большая часть затрат на формальные рассуждения перекладывается на плечи разработчиков приложений. - person MaD70; 28.10.2009
comment
w.r.t. гибкость и выразительность: нет, не думаю. Стандартный ML, Haskell, ATS и т. д. — это мощные языки программирования, на которых можно сжато написать любую программу. Разница в том, что они с самого начала представляют собой хорошо продуманные ЯП, а не надстройки на синтаксисе и семантике C. - person MaD70; 28.10.2009
comment
Почему DAG, а не дерево? Дерево также является DAG, в нем нет циклов, а циклы затрудняют анализ кода. - person Nils; 22.04.2014