On Sunday, September 8, 2019 at 10:17:20 PM UTC+2, Maciej Sobczak wrote:
> > 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)

Dlaczego warto wprowadzać takie rozróżnienie nazewnicze, dlaczego nie używać
określenia asercj a warunków weryfikacyjnych?

Pozdrawiam