> No to spróbujmy pierwszy przykład:
>
> /*@ ensures \result >= x && \result >= y;
> ensures \result == x || \result == y;
> */
> int max (int x, int y) { return (x > y) ? x : y; }
>
> int max (int x, int y) {
> int result = (x > y) ? x : y;
> assert(result >= x && result >= y);
> assert(result == x || result == y);
> return result;
> }
>
> Udało się.

Nie udało się, z czterech powodów.

Po pierwsze, asercje (nazwijmy je raczej warunkami weryfikacji) w tych przykładach są
właściwością deklaracji funkcji a nie jej ciała. Oznacza to, że są użyteczne zarówno
przy weryfikacji ciała funkcji jak i przy weryfikacji kodu wołającego. Twoje asserty
w ciele pełnią tylko tą pierwszą rolę, co je bardzo ogranicza.

Po drugie, warunki w komentarzach, gdzie są analizowane przez zewnętrzne narzędzie,
nie podlegają ograniczeniom języka C i mogą korzystać nie tylko z szerszej składni,
ale w ogóle z innego paradygmatu.

Po trzecie, na tym *pierwszym* przykładzie kończą się Twoje możliwości w tym
zakresie. Niezbyt imponująco. Dalsze przykłady są ciekawsze (co nawiązuje do
poprzedniego punktu).

Po czwarte wreszcie, Twoja wersja ma dead code. Mam nadzieję, że to nie wymaga
ponownego wyjaśnienia.

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