> Co to znaczy "poprawność programu"? Sprecyzuj.

Każdy student informatyki wie, że:
poprawność = częściowa poprawność + własność stopu + określoność obliczeń
gdzie częsciowa poprawność = zgodność z formalną specyfikacją

> Nigdy do końca nie wiadomo, czy program nie zawiera błedów.

No właśnie o to chodzi, że testami się tej pewności nie osiągnie, natomiast są
metody formalne, np. logika Hoare'a które taką pewność dają. Problem, w tym, że
są to metody pracochłonne i - przy bardziej skomplikowanych programach - trudne
matematycznie. Stąd całe moje pytanie: czy programiści wykorzystują je w
praktyce. Oczywiście są sytuacje kiedy dowód formalny poprawności jest bardzo
pożądany, np. gdy od poprawności programu zależy ludzkie życie.


--
Wysłano z serwisu OnetNiusy: http://niusy.onet.pl