В своей прошлой статье я описал процесс верификации примитивной функции на Си. Параллельно привел соображения, почему верификация Си кода недостаточна для того, чтоб считать программу безошибочной. В основном эти соображения сводятся к мысли, что написать код — это только часть истории о получении работающей программы. Следующим приближением к тому, чтобы получить действительно безошибочную программу, является верификация ассемблерных кодов, их уже не нужно будет транслировать и поэтому полностью исключится обширное поле для возникновения ошибок. В данной статье я опишу процесс доказательства некоторых свойств уже для ассемблерного кода, который на порядок примитивней, чем даже простейшая функция на Си, о которой говорилось в прошлой статье.
Читать полностью »
Рубрика «формальная верификаци»
Верификация программ на ARM ассемблере
2012-10-29 в 4:41, admin, рубрики: верификация, верификация программ, математика, Программирование, формальная верификаци, функциональное программирование, метки: верификация, верификация программ, формальная верификациФормальная верификация Си кода
2012-07-30 в 8:07, admin, рубрики: верификация, верификация программ, Программирование, формальная верификаци, метки: верификация, верификация программ, формальная верификаци Часто говорят что нет программ без ошибок. Это мнение сильно коробило мои эстетические чувства, поэтому я постарался поразбираться с формальной верификцией программ, ведь она обещает нам максимально возможную гарантию безошибочности при которой утверждение о корректности программы доказывается как математическая теорема. Здесь представлю результаты моего краткого ознакомления с этой темой.
Читать полностью »