> A konkretnie, co jest na temat a co nie jest i na jaki?

Pół dyskusji w tym wątku było nie na temat tego wątku.

> Nie wiem co to
> jest "verification condition".

To jest coś, co zakładamy[1], że jest prawdą albo co musi być wykazane[2], że jest
prawdą, żeby program uznać za poprawny.

[1] Przykładem takiego założenia jest np. zakres wartości typu int. Tego się nie
udowadnia, to się przyjmuje i dane z tego założenia są WEjściem dla innych rozważań.
[2] Przykładem takiego warunku jest np. to, co było pokazane dla funkcji max, albo
to, że funkcja sortująca faktycznie sortuje albo to, że funkcja abs nigdy nie zwróci
wartości ujemnej, itd. Takich rzeczy nie wiemy z góry, ale możemy je wykazać (albo im
zaprzeczyć) wnioskując na podstawie informacji, które już znamy.

Fachowo, dowiedzenie, że VC (verification condition) jest spełnione nazywa się
"discharge". Ale po polsku najlepiej powiedzieć, że jest "spełnione", bo
"rozładowywanie warunków" brzmi głupio. Dowody mogą być automatyczne albo ręczne.

I teraz ciekawostka: asercja napisana przy użyciu makra "assert" może być traktowana
jako warunek do wykazania *oraz* jako nowe założenie dla dalszych rozważań. W
niektórych językach do tego drugiego celu służy konstrukcja "assume" i stosuje się ją
wtedy, kiedy wiedza na jakiś temat pochodzi z zewnątrz - np. z tego, jak i gdzie dany
program jest użytkowany.

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