Языки, специально предназначенные для создания статической проверки легче
Много языков (возможно, все они) разработано для создания программ записи легче. Они все имеют различные домены и стремятся упрощать программы разработки в этих доменах (C, делает разрабатывающие программы низкого уровня легче, Java делает разрабатывающую сложную бизнес-логику легче, и др.). Возможно, другие цели принесены в жертву в пользе записи и поддержания программ в более легком, более естественном, меньшем количестве подверженного ошибкам пути.
Действительно ли там какие-либо языки специально предназначены для создания проверки исходного кода - т.е. статический анализ - легче? Конечно, возможность записать общие программы для современных машин должна также сохраниться.
6 ответов
Одной из целей разработки Ada была поддержка определенного объема формальной верификации. Это было в меру успешно, но верификация не получила того успеха, на который они рассчитывали. К счастью, Ada подходит для гораздо большего. К сожалению, это тоже не сильно помогло ей...
Существует подмножество Ada под названием Spark, которое поддерживает это сегодня. Praxis продает пакет разработки, построенный на его основе.
Я сам не использовал его, поэтому я не могу говорить с каким-либо авторитетом, но я понимаю, что язык программирования Eiffel был разработан для использования кода по контрактам, что значительно облегчит статический анализ Полегче. Я не знаю, считается это или нет.
У одного есть две проблемы при "выполнении проверки исходного кода проще ". Один из них - это языки, в которых вы не делаете грубых вещей, таких как произвольные случаи (например, C). Другой - с указанием того, что вы хотите проверить, для этого вам нужны хорошие языки утверждений.
Хотя многие языки предлагали такие языки утверждений, Я думаю, что сообщество EDA наиболее эффективно расширяет границы с временными спецификациями.«Язык спецификации свойств» является стандартом; дополнительные сведения см. в P1850 Standard for PSL: Property Specification Language (IEEE-1850) . Одна из идей, лежащих в основе PSL, заключается в том, что вы можете добавить его к существующим языкам EDA; Я думаю, что сообщество EDA со временем включилось в языки EDA.
Я часто хотел, чтобы что-то вроде PSL было встроено в обычное компьютерное программное обеспечение.
Существуют ли языки, специально разработанные для облегчения верификации исходного кода?
Это было смутной целью языков CLU и ML, но единственный известный мне язык, который серьезно относится к статической верификации, это Spark Ada.
Язык охраняемых команд Дейкстры (как описано в Дисциплине программирования) был разработан для поддержки статической верификации, но он явно не должен был быть реализован.
Язык Promela Жерара Хольцмана также был разработан для статического анализа программой проверки моделей SPIN, но опять же он не исполняемый.
Аудиторы на языке E предоставляют встроенные средства для написания анализа кода внутри самого языка и требуют, чтобы некоторые участки кода прошли некоторую статическую проверку. Возможно, вас также заинтересует относящаяся к теме работа.