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

do góry

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

Bo określenie "asercja" ma zbyt wiele znaczeń i u niektórych generuje chęć dyskusji
nie na temat. :-)

No i termin "verification condition" jest bardziej sexy, niż "assertion" i skupia
uwagę na temacie poprawności. Wpisz w Googlu jedno i drugie i porównaj wyniki. Od
razu widać, że "verification condition" jest bardziej na temat.
;-)

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

do góry

On 2019-09-08 22:17, Maciej Sobczak wrote:
> (nazwijmy je raczej warunkami weryfikacji)

Trafna nazwa!

AK

do góry

On Wednesday, September 11, 2019 at 9:21:07 AM UTC+2, Maciej Sobczak wrote:
> > > 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?
>
> Bo określenie "asercja" ma zbyt wiele znaczeń i u niektórych generuje chęć dyskusji
nie na temat. :-)
>
> No i termin "verification condition" jest bardziej sexy, niż "assertion" i skupia
uwagę na temacie poprawności. Wpisz w Googlu jedno i drugie i porównaj wyniki. Od
razu widać, że "verification condition" jest bardziej na temat.
> ;-)

A konkretnie, co jest na temat a co nie jest i na jaki? Nie wiem co to
jest "verification condition". Verification condition to te adnotacje, a
asercje to te marka/funkcje?

Pozdrawiam

do góry

> 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

do góry

On Thursday, September 12, 2019 at 9:21:42 AM UTC+2, Maciej Sobczak wrote:
> > 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.

Na razie rozumiem, że "verification condition" to jest cokolwiek z czego
prawdziwości wynika poprawność programu, albo czego prawdziwości jest
tożsama z poprawnością programu. Coś w rodzaju
X => Y
X <=> Y
Gdzie X to jest poprawny verification condition, a Y oznacza poprawność
programu.

Zwykle stosuję słabsze wnioskowanie, np. że z NIE prawdziwości warunków
testowych wynika że program jest nie 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ń.

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


> [2] Przykładem takiego warunku jest np. to, co było pokazane dla funkcji max,

Tak, tamto zrozumiałem, choć do składni w adnotacjach bym musiał przywyknąć.


> albo to, że funkcja sortująca faktycznie sortuje albo to, że
> funkcja abs nigdy nie zwróci wartości ujemnej, itd.

Abs i sortowanie stanowią stosunkowo łatwe przykłady. 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.


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

O jakie założenie i o jakie rozważania chodzi?

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

Nie używałem assume. Widzę że w C/C++ microsofcie coś dodali:
https://docs.microsoft.com/en-us/cpp/intrinsics/assu
me?view=vs-2019

A w GCC zalecają sztuczki:
https://stackoverflow.com/questions/25667901/assume-
clause-in-gcc
https://stackoverflow.com/questions/6031819/emulatin
g-gccs-builtin-unreachable

Nie rozumiem, jakie są korzyści z dodania pustej funkcji, albo z operacji
bitowej AND z samymi jedynkami:
x = x & (~0);

Chociaż bezpieczniej byłoby OR z zerami:
x = x | 0;

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

do góry

> 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

do góry