Математическая нотация концепций программирования
https://stackoverflow.com/questions/1632786
-
06-07-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
RussianВопрос
Существует много методов для представления структуры программы (например, диаграммы классов UML и т. д.). Мне интересно, есть ли соглашение, которое описывает программы строго математическим способом. Я особенно заинтересован в использовании математических обозначений для этой цели.
Пример : классы представлены в виде наборов (полей, свойств) и функций (работающих с элементами наборов). Родительский класс «поля являются подмножеством дочернего класса». Функции описаны в псевдокоде, который должен выглядеть примерно так ...
Решение
Я знаю, что Z-нотация в некоторой степени использовалась при формальной проверке программного обеспечения, например, проект Tokeneer .
Другие советы
Да, есть, Флойд -Лучная логика .
Есть много способов, но я думаю, что большинство из них неудобно для выражения структуры, поскольку структура часто не выражается в математических понятиях по умолчанию. Основным исключением являются, конечно, функциональные языки программирования. Подумайте о складках (катаморфизме), группах, алгебре и т. Д.
Для императивного программирования я знаю о существовании Z, который использует (чистую и расширенную) теорию множеств лямбда-исчисления и логику предикатов (первого порядка). Однако я не думаю, что это очень удобно. Единственным преимуществом использования математики для выражения структуры является тот факт, что вы можете доказать что-то об этом. Но если вы хотите сделать это, взгляните на JML, Spec # или Eiffel.
Зависит от того, чего вы пытаетесь достичь, но если вы пойдете по этому пути с использованием определенных языков, у вас могут возникнуть проблемы.
Например, см. обсуждение круговым эллипсом на C ++ FAQ Lite.
В этой книге применяется дедуктивный метод. программированию с помощью партнерских программ с абстрактным математическим теории, которые позволяют им работать. [...]
Я считаю, что Элементы программирования Александра Степанова и Пола МакДжонса очень близки к тому, что вы ищу.
Концепция - это описание требования к одному или нескольким типам заявлено с точки зрения существования и свойства процедур, тип атрибуты и функции типа определены на типах.
Z, о котором уже упоминалось, это почти то, что вы описываете. Есть несколько вариантов этого для объектно-ориентированного моделирования, но я думаю, что вы можете продвинуться далеко вперед с & Quot; стандартными Z's & Quot; схемы, если вы хотите моделировать классы.
Существует также Alloy , более новый и вдохновленный Z. Его обозначения, возможно, немного ближе к объекту -ориентация. Это также анализируемо, то есть вы можете проверить, какие модели вы создаете, удовлетворяют ли они определенным условиям, но это не может доказать, что свойства сохраняются, просто попытаться опровергнуть в пределах конечной области.
Статья Надежное программное обеспечение по дизайну представляет собой хорошее введение в Alloy. и тому подобное, наряду с таблицей доступных аналогичных инструментов.
Вы ищете функциональное программирование. Существует несколько функциональных языков программирования, и они все они основаны на фундаментальной математической теории, называемой лямбда-исчислением . Программы, написанные на функциональном языке программирования, таком как LISP, представляют собой математическое представление самих себя. ; -)
Существует математический язык, который на самом деле описывает программу или, скорее, ее операции. Вы берете исходное состояние и затем трансформируете это состояние, пока не достигнете желаемого целевого состояния. Преобразования дают программный код, который должен быть выполнен.
См. статью Википедии о логике Хоара .
Основная идея заключается в том, что для каждой функции (независимо от того, помещаете ли вы ее в класс или в функцию старого стиля), у вас есть предварительное и постусловие. Например, предварительным условием может быть наличие массива с элементами >= 0. постусловие состоит в том, что каждый элемент [i] должен быть < = element [j] для каждого i < = j.
Обычное описание будет " функция сортирует массив " ;. Но математические термины позволяют преобразовать входные данные (которые должны соответствовать предварительному условию) в выходные данные (которые должны соответствовать постусловию).
Это немного громоздко в использовании, особенно для более сложных программ, но некоторые примеры впечатляют. Часто в результате вы получаете действительно компактный код, который выглядит довольно сложным, но работает с первого раза.
Я бы хотел предложить Алгебру программирования . Это вычислительный подход к программам с использованием реляционной алгебры и Связи с Галуа .
Если у вас есть дальнейший интерес к этой теме, вы можете найти замечательную статью, здесь , автор Shin-Cheng Mu и Jos & # 233; Нуно Оливейра ( слайды ).
Использование реляционной алгебры и логики первого порядка также имеет хороший синергизм с Alloy , функциональным программированием и Проектирование по контракту (легко применяется для объектно-ориентированного программирования).
