|
ru.algorithms
- RU.ALGORITHMS ----------------------------------------------------------------
From : Boris Sivko 2:452/26.14 17 Apr 2003 20:40:26
To : Yurii Komov
Subject : Доказательство правильности ПО
--------------------------------------------------------------------------------
По данным контрразведки я узнал, что в Четверг Апрель 17 2003 15:49, Yurii
Komov писал Boris Sivko на тему "Доказательство правильности ПО":
BS>> Ищется любая информация по сабжу. Если кто интересовался данным
BS>> вопросом на серьёзном уровне, откликнетесь плз.
YK> Помнится, я писал в институте диплом "Доказательство правильности
YK> программ" - и программу, которая брала 2 простенькие программы (исх.
YK> тексты) и доказывала, что при любых исх. данных результат
YK> одинаков
Полный перебор?
YK> Самым "замечательным" результатом было то, что она доказала,
YK> что сортировка массива из 4-х элементов методом пузырька эквивалентна
YK> сортировке методом выбора макс. элемента Когда задал длину массивов 5
YK> - проработала больше суток, и я ее вырубил Процессор был тогда -
YK> Pentium133, что ли...
Ты получается доказал, что эти программы эквивалентны. А по идее нужно
например для всех входных A[1..n],n доказать, что на выходе будет A[i+1] >= A[i]
для i=1..(n-1).
Это ещё простая задача. В ней достаточно легко проверить правильность
требуемого постусловия. Вот если ты считаешь число pi с точностью до n-го знака,
то проверить так не удасться.
Счастливо, Yurii. Вспоминай обо мне...
... I'll be back...
* Origin: DOS_VID_анья, Из_WIN_и, если что... (2:452/26.14)
Вернуться к списку тем, сортированных по: возрастание даты уменьшение даты тема автор
|
Доказательство правильности ПО