32) Формальные методы доказательства правильности программ и их спецификаций. | MetodPro.ru

Реклама на сайте

32) Формальные методы доказательства правильности программ и их спецификаций.


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



Методические пособия

  • Системы автоматизированного проектирования
  • Социология молодёжи
  • Общая социология
  • Криптография
  • Проектирование трансляторов
  • Компьютерная графика
  • Моделирование систем
  • Информационная безопасность
  • Теория вычислительных процессов
  • Логические основы искусственного интелекта
  • Проектирование распределённых информационных систем