Эквивалентность между C/frama-c и Spark-ada
Я изучаю фреймворк Frama-c, и мне интересно, есть ли эквивалентность между C/Frama-c и Spark Ada. Я знаю, что может показаться странным сравнивать такие разные языки, но после прочтения статьи Дэвида А. Уилера, сравнения Йоханнеса Канига и небольшого руководства пользователя SPARK я с трудом догадываюсь, дают ли SPARK и C/Frama-c/ACSL такая же стойкость доказательства и та же надежность кода.
Заранее большое спасибо за высказанную точку зрения / опыт!
PS: я совсем новичок в frama-c и не очень разбираюсь в программировании на SPARK.
1 ответ
Я не знаю Frama-C, но доказательства SPARK - это, как я понимаю, абсолютные гарантии. С SPARK вы можете в какой-то степени выбрать, сколько вы хотите доказательств.
Основной уровень - доказать отсутствие ошибок времени исполнения (исключений), но SPARK попытается доказать все утверждения (включая предварительные и постусловия), которые вы вставляете в исходный текст. Поэтому, если вы вставляете утверждения, которые документируют некоторые функциональные требования, тогда гарантии (при условии, что ваши инструменты SPARK могут доказать правильность утверждений) распространяются на эти функциональные требования.