Эквивалентность между C / frama-c и Spark-ada

Question

Я изучаю фреймворк Frama-c, и мне интересно, есть ли эквивалентность между C / Frama-c и Spark Ada.Я знаю, что может показаться странным сравнивать такие разные языки, но после прочтения статьи Дэвида А. Уилера , сравнения Йоханнеса Канига и небольшого количества руководства пользователя SPARK я с трудомугадайте, дают ли SPARK и C / Frama-c / ACSL одинаковую стойкость доказательства и одинаковую надежность кода.

Заранее большое спасибо за вашу точку зрения / опыт!

PS: Я совсем новичок в frama-c и мало что знаю о программировании на SPARK.

Answer 1

Я не знаю Frama-C, но SPARK-доказательства - это, как я понимаю, абсолютные гарантии.С SPARK вы можете в какой-то степени выбрать, сколько вы хотите доказательств.

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