🚀 go-pugleaf

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/assume?view=vs-2019

A w GCC zalecają sztuczki:
https://stackoverflow.com/questions/25667901/assume-clause-in-gcc
https://stackoverflow.com/questions/6031819/emulating-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