|
|
|
|
|
|
|
|
|
|
верны". Верификация более длинной программы показывает, что программа обладает некоторыми свойствами (например, никогда не выдает неуместные сообщения). Эта программа может неверно работать в других случах, но такое доказательство гарантирует, что определенные ошибки не могут быть сделаны. Еще один недостаток - это высокая стоимость: производительность одного программиста составляла только несколько команд в день (две - в коротких программах, четыре - в длинных). Дальнейшие иследования должны повысить производительность, но даже такая высокая стоимость приемлема для прикладных задач, где нужна высокая надежность или от которых зависит жизнь людей. Относительно перспектив верификации программ для таких прикладных задач я настроен оптимистически. Чтобы больше узнать о системе Gypsy, читайте статью Гуда (Good. Mechanical proofs about computer programs) в Phil. Trans. R. Soc. London A 312, p. 389 - 409 (1404).
|
|
|
|
|
|
|
|
|
|
