Математическая нотация концепций программирования

Question

Существует много методов для представления структуры программы (например, диаграммы классов UML и т. Д.). Мне интересно, есть ли соглашение, которое описывает программы строго математическим способом. Я особенно заинтересован в использовании математических обозначений для этой цели.

Пример : классы представлены в виде наборов (полей, свойств) и функций (работающих с элементами наборов). Родительский класс «поля являются подмножеством дочернего класса». Функции описаны в псевдокоде, который должен выглядеть так и так ...

Answer 1

Я знаю, что Z Notation использовалась в некоторой степени при формальной проверке программного обеспечения, например, проект Tokeneer .

Z Обозначение

Z Справочное руководство

Answer 2

http://www.amazon.com/Concrete-Mathematics-Foundation-Computer-Science/dp/0201558025

Answer 3

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

Answer 4

Z, о котором уже упоминалось, это в значительной степени то, что вы описываете. Есть несколько вариантов этого для объектно-ориентированного моделирования, но я думаю, что вы можете продвинуться довольно далеко со схемами "стандартного Z", если вы хотите моделировать классы.

Существует также Alloy , который является более новым и вдохновлен Z. Его обозначения, возможно, немного ближе к объектной ориентации. Он также анализируем, то есть вы можете проверить созданные вами модели на предмет их соответствия определенным условиям, но он не может доказать, что свойства сохраняются, просто попытаться опровергнуть в пределах конечной области.

Статья Надежное ПО от Design * - хорошее введение в Alloy и тому подобное, наряду с таблицей доступных аналогичных инструментов.

Answer 5

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

Я считаю, что Элементы программирования Александра Степанова и Пола МакДжонса, очень близки к тому, что вы ищете.

Concepts

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

Answer 6

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

Например, см. Обсуждение круг-эллипс на C ++ FAQ Lite.

Answer 7

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

Для императивного программирования я знаю о существовании Z, который использует (чистую и расширенную) теорию множеств лямбда-исчисления и логику предикатов (первого порядка). Однако я не думаю, что это очень удобно. Единственным преимуществом использования математики для выражения структуры является тот факт, что вы можете доказать что-то об этом. Но если вы хотите сделать это, взгляните на JML, Spec # или Eiffel.

Answer 8

Да, есть, Floyd-Hoare Logic .

Answer 9

Я хотел бы предложить Алгебра программирования . Это вычислительный подход к программам с использованием реляционной алгебры и соединений Галуа .

Если у вас есть дальнейший интерес к этой теме, вы можете найти удивительную статью здесь Шин-Ченг Му и Хосе Нуно Оливейра ( слайды ).

Использование реляционной алгебры и логики первого порядка также имеет хорошую синергию с Alloy , Функциональным программированием и Проектированием по контракту (легко применяется для объектно-ориентированного программирования).

Answer 10

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

См. Статью Википедии о логике Хоара .

Основная идея заключается в том, что для каждой функции (независимо от того, помещаете ли вы ее в класс или в функцию старого стиля), у вас есть предварительное и постусловие. Например, предварительным условием может быть наличие массива, содержащего >= 0 элементов. постусловие состоит в том, что каждый элемент [i] должен быть равен <= element [j] для каждого i <= j. </p>

Обычное описание будет "функция сортирует массив". Но математические термины позволяют преобразовать входные данные (которые должны соответствовать предварительному условию) в выходные данные (которые должны соответствовать постусловию).

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