On 17 Sie, 13:01, j...@p...onet.pl wrote:

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

To zależy, gdzie student studiował.

http://en.wikipedia.org/wiki/Partial_correctness

Częściowa poprawność oznacza, że JEŚLI program w ogóle da jakieś
wyniki, to będą one poprawne. W szczególności częściowa poprawność nie
chroni przed zapętleniem się.

> 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.

Tak. Jednym z ciekawszych rozwiązań w tym zakresie jest SPARK:

http://en.wikipedia.org/wiki/SPARK

Jest ciekawy dlatego, że będąc podzbiorem znanego już języka
imperatywnego jest też od razu kompilowalny do kodu wynikowego. To nie
są jakieś obrazki czy inne matematyczne robaczki, tylko żywy kod z
dodatkową specyfikacją nt. przepływu informacji czy pre/post-
conditions. Weryfikuje się taki kod odpowiednimi narzędziami a potem
wrzuca do normalnego kompilatora i działa. Sporo tym można zrobić i
nawet się tego używa w praktyce a ponieważ kompletny zbiór narzędzi
jest dostępny za friko, to jest to też dobra platforma dla samouków.

> Oczywiście są sytuacje kiedy dowód formalny poprawności jest bardzo
> pożądany, np. gdy od poprawności programu zależy ludzkie życie.

Nadal pozostaje pytanie o poprawność specyfikacji. Można spokojnie
udowodnić poprawność źle wyspecyfikowanego programu - program będzie
idealnie robił nie to, co trzeba. Niestety zawsze gdzieś będzie
miejsce na czynnik ludzki jako najsłabsze ogniwo.

--
Maciej Sobczak * http://www.inspirel.com