W dniu środa, 1 kwietnia 2015 11:57:13 UTC+2 użytkownik M.M. napisał:

> > > > "Najlepiej jak to możliwe" -- to też nieprecyzyjne określenie.
> > > > Można je rozumieć jako "najlepiej jak komputer potrafi", albo
> > > > "najlepiej jak programista potrafi". To ostatnie jest zresztą
> > > > zazwyczaj twardym limitem, chyba że klient znajdzie lepszego
> > > > programistę
> > > No oczywiście że jest nieprecyzyjne. Jest nieprecyzyjne jak każde
> > > generalizowanie.
> >
> > Generalizowanie to tyle, co uogólnianie, czyli przechodzenie
> > od przypadku konkretniejszego do ogólniejszego. Stąd, że Twoje
> > generalizowanie jest nieprecyzyjne, nie wynika, że każde generalizowanie
> > jest nieprecyzyjne.
> Poczekaj bo się robią jakieś jaja z tej rozmowy:) Wątek ten dotyczy
> (nie)przydatności formalnego dowodu na poprawność programu w
> praktyce programistycznej/biznesowej. Potem ja wtrąciłem, że
> wymagania są różne, np. klient chce najlepszy program. Jak słuszne
> zauważyłeś, nie precyzowałem co oznacza najlepszy. Piłem do tego,
> że jeśli już tak ściśle i formalnie chcemy dowodzić, to należało
> by również dowieść, że program istotnie jest najlepszy. Więc moje
> generalizowanie obejmuje zbiór kryteriów według których
> w praktyce programistycznej ocenia się programy. Co widzisz
> nieprecyzyjnego w takim generalizowaniu?

To Ty (nie ja) napisałeś, cytuję "[określenie >najlepiej<] jest
nieprecyzyjne jak każde generalizowanie", stwierdzając
tym samym, że każde generalizowanie jest nieprecyzyjne.

> > Na przykład dodanie funkcji porównującej jako parametru
> > dla funkcji "sort" jest generalizowaniem, a jest piekielnie
> > precyzyjne.
> Dlaczego można precyzyjne generalizować po tejże funkcji, a po
> spotykanych kryteriach oceny programu nie można?

Nie wiem. To Ty twierdzisz, że nie można precyzyjnie generalizować
(chyba że coś źle zrozumiałem, bo teraz wydajesz się sugerować,
że jednak można?)

> > > Przypuszczasz, że chodziło mi o dowód formalny (na podstawie kodu
> > > źródłowego) na istnienie lepszego programu na rynku? ;-)
> >
> > Problem polega na tym, że nie wiem, o co Ci chodziło, bo wyraziłeś
> > się dość nieprecyzyjnie
> Myślałem że jak tylko odrzucisz przypadki nonsensowne, to będzie
> precyzyjnie.

Jak odrzuciłem przypadki nonsensowne, to wyszedł mi zbiór pusty.

> > W pewnym zakresie może tak. Ale znajdzie się również taki, w którym
> > eksperci będą między sobą dywagować, czy Słomczyński, czy Barańczak
> TO też da się rozwiązać, można uznać za takie same, jeśli eksperci od
> razu nie są jednoznaczni - ale nie ma sensu brnąć dalej.

I w ten sposób może się okazać, że nie zabrniemy za daleko.

> > Też nie wiem. Prawdopodobnie nie można, tym bardziej, że
> > nie umiemy nawet uściślić, co to znaczy "lepiej tłumaczyć tekst"
> No więc właśnie. Co z tego, że nawet jeśli są jakieś znikome
> szanse na udowodnienie poprawności programu, to zwykle nie ma
> żadnych szans, czy program, choć jest poprawny, to realizuje
> zamierzony cel.

Pytanie, które chcemy sobie zadać, brzmi: w jakim zakresie
istnieje potrzeba udowodnienia tego, że program zachowuje
określone niezmienniki? Podane przez Ciebie przykłady całkowicie
chybiają. Koledzy podają przykłady np. sterowników hamulców
w samochodzie. Inny prosty przykład, to udowodnić, że urządzenie
odpowiedzialne za zmianę świateł na skrzyżowaniu nie dopuści
nigdy do tego, że dla obu kierunków skrzyżowania nie będzie
się paliło jednocześnie zielone światło.

> > Ale niestety Twoje użycie słowa "najlepszy" jest nieprecyzyjne,
> > bo "najlepszy" może być również w sensie "maintainability" -- że
> > ma najlepsze komentarze, jest najłatwiej rozszerzalny itd.
> Oczywiście że może. Przecież to jest bardzo często spotykany
> wymóg. Ja np. mam sprzeczne wymogi: program ma być wydajny, ma
> obsługiwać bardzo dużą ilość użytkowników na tanim sprzęcie i
> jednocześnie ma być bardzo podatny na zmiany, żeby szybko go
> rozbudowywać.

A gdzie jest ta sprzeczność?

> > > > Nieprawda. To, jak się coś skonkretyzuje (oraz co się skonkretyzuje),
> > > > ma kluczowe znaczenie dla łatwości/trudności przeprowadzenia dowodu.
> > > Może czegoś nie wiem, dla jakich kryteriów dowód będzie łatwy w
> > > przeprowadzeniu?
> >
> > Nie rozumiem o co pytasz. W ogólności zależy to od przypadku.
> Pytam o to, jakie miałeś na myśli przypadki, gdy pisałeś, że
> może dowód być łatwy.

Na przykład wspominany przeze mnie przypadek, że funkcja append
jest operatorem łącznym.

> > > > owo polecenie. Deadlocka otrzymamy w każdym przypadku, gdy którykolwiek
> > > > z wątków w danej jednostce uruchomieniowej nie wywoła polecenia
__syncthreads().
> > > Nigdy nie używałem tego polecenia. Czy jest konieczne używanie?
> > > Co ono usprawnia?
> >
> > Umożliwia synchronizację wątków przed dostępem do pamięci.
> Po to jest prawie każda synchronizacja, a jeśli słowo pamięć
> zmienimy na zasób, to chyba dosłownie każda.

No widzisz.

> > Jeśli Cię to bardziej interesuje, polecam kurs z "Heterogenous Parallel
> > Programming" na Courserze albo książkę "CUDA w przykładach" (wyd. Helion)
> Nie mam aż tyle czasu, myślalem że rzucisz kilka zalet.

Zalet synchronizacji wątków przed dostępem do pamięci?

> > Nie. Każdy wątek może bezpiecznie wywołać __syncthreads i nie ma potrzeby
> > zabezpieczania jej semaforami,
> Nie pisałem że trzeba ją zabezpieczać semaformai, tylko że trzeba ją
> traktować jakby była zabezpieczona według takiego schematu.

I co to nam daje, w sensie udowodnienia, że program nie ma deadlocka?