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