M>Это все здорово, но практика такова, что доказательное программирование возможно только в очень редких ситуациях.
Есть большое количество formally verified software. Есть формальная верификация моделей.
Это все не так уж сложно, если разобраться. В конце концов, есть же просто мощные способы тестирования, которые не являются формальным доказательством, но проведены на существенную глубину цепочек смены состояний.
Здравствуйте, SkyDance, Вы писали:
M>>Это все здорово, но практика такова, что доказательное программирование возможно только в очень редких ситуациях.
SD>Есть большое количество formally verified software. Есть формальная верификация моделей.
Они все работают хорошо, пока не нужно взаимодействовать с внешним миром, который формальной верификации не поддаётся. Чем меньше внешнего мира, тем лучше работают формализмы, и тем хуже практическая применимость.
S>Они все работают хорошо, пока не нужно взаимодействовать с внешним миром, который формальной верификации не поддаётся. Чем меньше внешнего мира, тем лучше работают формализмы, и тем хуже практическая применимость.
Внешний мир верифицировать не требуется.
Достаточно предоставить формальный протокол взаимодействия.
Здравствуйте, SkyDance, Вы писали:
S>>Они все работают хорошо, пока не нужно взаимодействовать с внешним миром, который формальной верификации не поддаётся. Чем меньше внешнего мира, тем лучше работают формализмы, и тем хуже практическая применимость.
SD>Внешний мир верифицировать не требуется. SD>Достаточно предоставить формальный протокол взаимодействия.
Достаточно для того, чтобы верифицировать программу, но обычно не достаточно для работы с миром.
vaa>Экспериментальное тестирование программ
vaa>может служить для доказательства наличия ошибок,
vaa>но никогда не докажет их отсутствия.
Логично. И что? Вывод какой? Как в классиках?
Лозунг у них был такой: «Познание бесконечности требует бесконечного времени». С этим я не спорил, но они делали из этого неожиданный вывод: «А потому работай не работай — все едино».
Здравствуйте, fmiracle, Вы писали:
F>Здравствуйте, vaa, Вы писали:
vaa>>
vaa>>Экспериментальное тестирование программ
vaa>>может служить для доказательства наличия ошибок,
vaa>>но никогда не докажет их отсутствия.
F>Логично. И что? Вывод какой? Как в классиках?
алгоритм должен строится на четких утверждениях
иначе начинается гадание на кофейной гуще тестирование
тут кончено зависит многое от инструмента(например F#) и культуры(швейцарская школа программирования)
let pal (word:string) =
let rec loop a =
match a with
| [] | [_] -> true
| x -> (x[0] = x[x.Length - 1]) && (if x.Length < 4 then true else (loop x[1 .. x.Length - 2]))
loop [for c in word -> c]
