Языки, специально разработанные для упрощения статической проверки

Question

Многие языки (возможно, все) предназначены для облегчения написания программ. Все они имеют разные домены и стремятся упростить разработку программ в этих доменах (C облегчает разработку низкоуровневых программ, Java облегчает разработку сложной бизнес-логики и др.) Возможно, другие цели приносятся в жертву ради написания и поддержки программ более простым, естественным и менее подверженным ошибкам способом.

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

Answer 1

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

Есть подмножество Ada под названием Spark , которое поддерживает это сегодня. Praxis продает комплект разработки, построенный вокруг него.

Answer 2

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

Answer 3

Существуют ли какие-либо языки, специально разработанные для облегчения проверки исходного кода?

Это была неопределенная цель для языков CLU и ML, но единственный известный мне языковой дизайн, который действительно серьезно относится к статической проверке, - это Spark Ada.

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

Язык Promela Джерарда Хольцмана также был разработан для статического анализа с помощью средства проверки модели SPIN, но, опять же, он не исполняемый.

Answer 4

У одного есть две проблемы в «облегчении проверки исходного кода». Одним из них являются языки, на которых вы не делаете грубые вещи, такие как произвольные случаи (например, C). Другим является указание того, что вы хотите проверить, для этого вам нужны хорошие языки утверждений.

Хотя многие языки предлагают такие языки утверждений, Я думаю, что сообщество EDA наиболее эффективно продвигает конверт с временными спецификациями. «Язык спецификации свойств» является стандартом; Вы можете узнать больше из P1850 Standard для PSL: Язык спецификации свойств (IEEE-1850) . Одна из идей PSL заключается в том, что вы можете добавить его к существующим языкам EDA; Я думаю, что со временем сообщество EDA включается в языки EDA.

Мне часто хотелось, чтобы что-то вроде PSL было встроено в обычное компьютерное программное обеспечение.

Answer 5

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

Answer 6

Существует SAIL , промежуточный язык статического анализа или Flexibo

Answer 7

Статическая проверка - плохое начало для этой задачи.Он основан на предположении, что можно автоматически проверить правильность программы.В реальности это невозможно, и ожидать, что программа проверит произвольно сложный код без каких-либо подсказок, просто глупо.Обычно программное обеспечение для статической проверки в конечном итоге требует подсказок по всему исходному коду, и в конце концов генерирует множество ложных срабатываний и ложных отрицаний.У него есть своя ниша, но это все.(См. Введение к « Типам и языкам программирования » Пирса)

В то время как инструменты такого типа были разработаны инженерами для их собственных простых целей, в академии выпекается настоящее решение.Было обнаружено, что типы в статически типизированных языках программирования эквивалентны логическим утверждениям, если все идет гладко и язык не имеет какого-то плохого поведения.Это называется " соответствие Карри-Ховарда ", а встраивание логики в типы - это " логика Брауэра-Хейтинга-Колмогорова ".Самые мощные доказательства возможны только в языках с мощными типами: зависимые типы .Если мы на время забудем всю эту терминологию, это означает, что мы можем написать программы, которые несут доказательства своей собственной корректности, и эти доказательства проверяются во время компиляции программы, при этом в случаеошибка.

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

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

Существует ряд языков с типизированной зависимостью для различных целей: Coq , Агда , Идрис , Эпиграмма , Кайен и т. Д.

Тактика реализована на Coq и, возможно, еще на нескольких языках.Кроме того, Coq является наиболее зрелым из них, с инфраструктурой, включающей такие библиотеки, как Bedrock .

В случае, если извлечения кода C из Coq недостаточно для ваших требований, вы можете использовать ATS, что соответствует по производительности с C.

Haskell использует слабую форму соответствия Карри-Ховарда: она отлично работает, если только вы не начинаете писать программы с ошибками или с зацикливанием.Если вам не сложно написать формальные доказательства, рассмотрите возможность использования Haskell.