ВУЗ:
Составители:
Рубрика:
17
Рис. 2. Три канала вывода
1.2.3. Метод Флойда и утверждения Assert
Лет двадцать назад большие надежды возлагались на формальные методы
доказательства правильности программ, позволяющие доказывать корректность
программ аналогично доказательству теорем. Реальные успехи формальных до-
казательств невелики. Построение такого доказательства не проще написания
корректной программы, а ошибки столь же возможны и часты, как и ошибки
программирования. Тем не менее, эти методы оказали серьезное влияние на
культуру проектирования корректных программ, появление в практике про-
граммирования понятий предусловия и постусловия, инвариантов и других
важных понятий.
Одним из методов доказательства правильности программ был метод
Флойда, при котором программа разбивалась на участки, окаймленные утвер-
ждениями – булевскими выражениями (предикатами). Истинность начального
предиката должна была следовать из входных данных программы. Затем для
каждого участка доказывалось, что из истинности предиката, стоящего в начале
Страницы
- « первая
- ‹ предыдущая
- …
- 15
- 16
- 17
- 18
- 19
- …
- следующая ›
- последняя »
