> Zwykle stosuję słabsze wnioskowanie, np. że z NIE prawdziwości warunków
> testowych wynika że program jest nie poprawny.

Więc uściślijmy: chodzi o poprawność względem tych warunków, które zostały określone.
Czyli jeśli ktoś nie napisał jakiegoś ważnego warunku weryfikacji, to nie może mieć
pretensji, że program jest niepoprawny chociaż wszystkie warunki (te niekompletne) są
spełnione i narzędzie mu powiedziało, że jest 0 errors, 0 warnings.

Ale też nikt nie twierdzi, że całe zjawisko poprawności należy tak pokryć. Na
weryfikację składają się analizy, przeglądy i testy. Warunki poprawności należą do
analiz i jeśli nie są kompletne, to uzupełniamy w pozostałych dwóch. Oczywiście, fani
metod formalnych dążą do tego, żeby analiza miała jak największy zakres, bo wtedy
można oszczędzić gdzie indziej (na testach).

> Tak, to chyba wynika z prawdziwości zdania "kompilator nie ma błędów".

Tak, to ciekawa uwaga. Jeżeli zakładamy, że kompilator może mieć błędy, to analizy
kodu źródłowego nie wystarczają, i tak trzeba mieć komplet testów (i to jest argument
przeciwko analizom).

> do składni w adnotacjach bym musiał przywyknąć.

Jak do każdej innej. Faktem jest, że ASCII nie bardzo ma coś do zaoferowania gdy w
grę wchodzą bardziej skomplikowane zapisy i się robi sieczka. Dlatego osobiście widzę
tu miejsce na integrację z narzędziami takimi jak Mathematica.

> Abs i sortowanie stanowią stosunkowo łatwe przykłady.

Sortowanie to jeden z najtrudniejszych przykładów w ogóle. Nie wystarczy pokazać, że
elementy są w dobrej kolejności, trzeba jeszcze pokazać, że to są właściwe elementy
(że żaden nie zginął albo nie pojawił z czapy).

> Zwykle nie wiem
> jak mam zrobić warunki, gdy mam okienko dialogowe np. z 20ma polami i
> piszę parser czy użytkownik nie wpisał blędnych wartości? Czy parser
> przepuści jakiś przypadek błędnych danych wejściowych dla programu?
> Niby sam parser jest takim warunkiem, działa na zasadzie: dane złe, to
> warunek je wychwyci.

Dobry przykład. Wtedy można zmienić myślenie z "wychwyć złe wartości" na "akceptuj
dobre wartości", czasem to ułatwia projektowanie.

> > 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ń.
>
> O jakie założenie i o jakie rozważania chodzi?

void foo()
{
// część 1
// ...

assert(x > 0); // VC_1

// część 2
// ...

assert(x > 0); // VC_2
}

Pierwszy warunek sprawdza, czy część 1 jest poprawna a drugi warunek sprawdza część
2. Ten drugi warunek polega na wiedzy (założeniu) z warunku pierwszego, czyli
zakładamy, że na początku części 2 jest x > 0, bo mamy taką "gwarancję". I jeśli z
części 2 wynika, że *przy takim założeniu nadal* jest x > 0, to wtedy cieszymy się,
że część 2 jest poprawna.

I teraz może się okazać, że nie umiemy wykazać VC_1, bo jest to zbyt trudne
(powiedzmy, że wtedy pokrywamy to testami). Ale jeśli VC_2 jest spełnione, to nadal
wiemy, że część 2 jest poprawna.
To jest forma długu technicznego, bo jeśli się okaże (np. w testach), że jednak część
1 jest niepoprawna, to nasza analiza części 2 jest nic nie warta, bo opierała się na
błędnych założeniach. Ale taki dług można podjąć i tak się robi.

Oczywiście mówimy o analizach statycznych, nie o run-time'owym assercie.

> Nie używałem assume.

Bo w run-time to nie ma sensu, więc tego normalnie w C/C++ nie ma.
Ale zobacz tutaj:

https://docs.adacore.com/spark2014-docs/html/ug/en/s
ource/assertion_pragmas.html#pragma-assume

Assume piszemy wtedy, gdy wiemy coś, czego w kodzie nie widać.

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