Исходное сообщение
"Найден способ формального подтверждения соответствия ПО техн..." Отправлено Aleksey, 14-Авг-09 15:15
Выдержка из с их страницы (statistic): ======= Сколько строк было проверено? > 7500 строк на C. Пока не проверен эсемблерный код и код, ответственный за загрузку (1200 строк) Насколько большое получилось доказательство? Около 200000 строк кода на языке доказательств Isabelle. Весь код доказательства был написан вручную с последующей машинной проверкой. В сумме это приблизительно 3500 страниц формата A4, если его распечатать (высота распечатки будет около полуметра высотой). Это одно из самых больших формальных доказательств из когда-либо сделаных. Для примера, известная теорема о четырех красках (которая тоже была доказана машиной) состояла из 60000 строк в доказательстве теоремы. Единственное известное доказательство, которое больше этого принадлежит проекту Verisoft (они сообщают о 245000 строк доказательства). И конечно, в математике, чем меньше доказательство, тем оно понятнее :) ======= Так что ни о каком прорыве в программировании речи не идет.