Многие языки (возможно, все они) предназначены для упрощения написания программ. Все они имеют разные домены и направлены на упрощение разработки программ в этих областях (C упрощает разработку программ на низком уровне, Java упрощает разработку сложной бизнес-логики и т.д.). Возможно, другие цели приносятся в жертву ради написания и поддержания программ более простым, более естественным, менее подверженным ошибкам способом.
Существуют ли какие-либо языки, специально предназначенные для проверки исходного кода - т.е. статический анализ - проще? Разумеется, также необходимо сохранить возможность писать общие программы для современных машин.
Одной из целей дизайна Ada было поддержание сертифицированной суммы формальной проверки. Это было умеренно успешным, но проверка точно не взлетела, как они надеялись. К счастью, Ада хороша гораздо больше. К сожалению, это тоже не помогло...
Там есть подмножество Ada, называемое Spark, которое сохраняет это в живых сегодня. Praxis продает встроенный пакет разработки.
Существуют ли какие-либо языки, специально предназначенные для облегчения проверки исходного кода?
Это была неопределенная цель как CLU, так и языков ML, но единственный язык, который я знаю, который действительно статично проверяет, - это Spark Ada.
Язык Dijkstra охраняемых команд (как описано в Discipline of Programming) был разработан для поддержки статической проверки, но он явно не предполагался реализованным.
Язык Gerard Holzmann Promela также был разработан для статического анализа с помощью проверки модели SPIN, но опять же не исполнялся.
Auditors на языке E предоставляет встроенное средство написания анализов кода в самом языке и требует, чтобы какой-либо раздел код проходит некоторую статическую проверку. Вы также можете быть заинтересованы в соответствующей части статьи.
Существует SAIL, промежуточный язык статического анализа или Flexibo
Я не использовал его сам, поэтому я не могу говорить с какими-либо полномочиями, но я понимаю, что язык программирования Эйфеля был разработан для использования Code by Contracts, что упростило бы статический анализ. Я не знаю, имеет ли это значение или нет.
У одного есть две проблемы: "упростить проверку исходного кода". Один - это языки, на которых вы не делаете грубые вещи, такие как произвольные случаи (например, C). Другой указывает, что вы хотите проверить, для этого вам нужны хорошие языки утверждений.
Хотя многие языки предлагали такие языки утверждений, Я думаю, что сообщество EDA максимально эффективно использует конверт с временными характеристиками. "Язык спецификаций свойств" является стандартом; вы можете узнать больше из P1850 Standard для PSL: язык спецификации свойств (IEEE-1850). Одна идея PSL заключается в том, что вы можете добавить ее к существующим языкам EDA; Я думаю, что сообщество EDA с течением времени включилось в EDA langauges.
Я часто хотел, чтобы что-то вроде PSL было встроено в обычное компьютерное программное обеспечение.
Статическая проверка является плохим началом для этой задачи. Это основано на предположении, что можно проверить правильность программы автоматически. Это невозможно в реальном мире, и ожидать, что программа проверяет произвольно сложный код без каких-либо намеков, просто тупо. Обычно программное обеспечение для статической проверки заканчивается тем, что требует намеков по всему исходному коду и в итоге генерирует множество ложных срабатываний и ложных негативов. У этого есть некоторая ниша, но что это. (См. Введение в " Типы и языки программирования" Пирсом)
Несмотря на то, что эти инструменты были разработаны инженерами для своих простых целей, реальное решение выпекалось в академии. Было обнаружено, что типы в статически типизированных языках программирования эквивалентны логическим утверждениям, учитывая, что все идет гладко, а язык не имеет своего рода плохого поведения. Это называется "" Карри-Говардская переписка", а вложение логики в типы " Логика Брауэра-Хейтинга-Колмогорова ". Наиболее мощные доказательства возможны только на языках с мощными типами: зависимые типы. Если мы забудем всю эту терминологию какое-то время, это означает, что мы можем написать программы, которые несут доказательства своей собственной корректности, и эти доказательства проверяются в то время как программа компилируется, без исполняемого файла, указанного в случае сбоя.
Положительная сторона этого подхода заключается в том, что вы никогда не получите ложные негативы, то есть скомпилированная программа будет работать правильно в соответствии со спецификацией, Даже без дополнительных доказательств в отношении спецификаций программы на языках с зависимым от языка менее подвержены ошибкам, поскольку деления на ноль, необработанные исключения и переполнения никогда не заканчиваются в исполняемой программе.
Всегда писать такие доказательства вручную - утомительно. Для этого существуют " тактика", то есть программы, которые генерируют доказательства правильности. Они почти эквивалентны программам для статической проверки, но, в отличие от них, необходимы для создания формальных доказательств.
Существует ряд языков с зависимым языком для разных целей: Coq, Agda, Idris, Epigram, Cayenne и т.д.
Тактика реализована в Coq и, возможно, на нескольких языках. Также Coq является наиболее зрелым из всех, с инфраструктурой, включая библиотеки, такие как Bedrock.
В случае, если извлечение кода C из Coq недостаточно для ваших требований, вы можете использовать ATS, что на уровне производительности с C.
Haskell использует слабую форму соответствия Карри-Говарда: он отлично работает, если вы не начинаете писать неудачные или навсегда запутывающие программы. Если ваши требования не так уж трудны для написания формальных доказательств, рассмотрите возможность использования Haskell.