Pytania otagowane jako correctness-proof

Pytania, które dotyczą dowodów poprawności algorytmów.

29
Dlaczego zapisywanie dowodów matematycznych jest bardziej odporne na błędy niż pisanie kodu komputerowego?
Zauważyłem, że o wiele łatwiej jest mi zapisać matematyczne dowody bez popełniania błędów niż napisać program komputerowy bez błędów. Wydaje się, że jest to coś bardziej rozpowszechnionego niż tylko moje doświadczenie. Większość ludzi cały czas popełniają błędy w oprogramowaniu i mają kompilator, który cały czas mówi im, jaki jest błąd. …
13
Jak oszukać heurystykę „wypróbuj niektóre przypadki testowe”: Algorytmy, które wydają się prawidłowe, ale w rzeczywistości są nieprawidłowe
Aby spróbować sprawdzić, czy algorytm dla jakiegoś problemu jest prawidłowy, zwykle punktem wyjścia jest próba uruchomienia algorytmu ręcznie na kilku prostych przypadkach testowych - wypróbuj go na kilku przykładowych przypadkach problemów, w tym na kilku prostych „przypadkach narożnych” „. To świetna heurystyka: to świetny sposób na szybkie wyeliminowanie wielu niepoprawnych …
2
Jak udowodnić, że chciwy algorytm jest poprawny
Mam chciwy algorytm, który, jak podejrzewam, może być poprawny, ale nie jestem pewien. Jak sprawdzić, czy jest poprawny? Jakich technik należy użyć do udowodnienia, że ​​chciwy algorytm jest poprawny? Czy istnieją wspólne wzorce lub techniki? Mam nadzieję, że stanie się to pytaniem referencyjnym, które można wykorzystać do wskazania początkującym; stąd …
1
Jak udowodnić poprawność algorytmu losowego?
Mam dwa sposoby tworzenia listy przedmiotów w losowej kolejności i chciałbym ustalić, czy są one równie uczciwe (obiektywne). Pierwszą metodą, której używam, jest skonstruowanie całej listy elementów, a następnie wykonanie losowania (powiedzmy losowanie Fisher-Yates). Druga metoda jest raczej metodą iteracyjną, która utrzymuje losowość listy przy każdym wstawieniu. W pseudokodzie funkcja …
5
Przykład algorytmu bez dowodu poprawności
Mamy logikę Hoare'a. Dlaczego wciąż jest możliwe, że algorytm ma rację, ale nie ma dowodów na jego poprawność? Załóżmy, że algorytm jest wyrażony w C. Następnie możemy argumentować krok po kroku, że robi to, co powinien. Więc moje pytanie brzmi: Podaj przykład algorytmu, który jest odpowiedni, ale nie ma dowodu …
6
Znalezienie maksymalnego XOR dwóch liczb w przedziale: czy możemy zrobić coś lepszego niż kwadratowy?
Załóżmy, że otrzymaliśmy dwie liczby i i że chcemy znaleźć dla l \ le i, \, j \ le r .lllrrrmax(i⊕j)max(i⊕j)\max{(i\oplus j)}l≤i,j≤rl≤i,j≤rl\le i,\,j\le r Naiwny algorytm sprawdza po prostu wszystkie możliwe pary; na przykład w rubinie mielibyśmy: def max_xor(l, r) max = 0 (l..r).each do |i| (i..r).each do |j| if …
3
Próbuję zrozumieć ten dowód poprawności Quicksort
Ten dowód jest dowodem indukcyjnym i wygląda następująco: P (n) jest twierdzeniem, że „Quicksort poprawnie sortuje każdą tablicę wejściową o długości n”. Przypadek podstawowy: każda tablica wejściowa o długości 1 jest już posortowana (blokada P (1)) Krok indukcyjny: fix n => 2. Napraw niektóre tablice wejściowe o długości n. Trzeba …
6
Czy techniki weryfikacji programu mogą zapobiec występowaniu błędów w gatunku Heartbleed?
W sprawie błędu Heartbleed Bruce Schneier napisał w swoim Crypto-Gram z 15 kwietnia: „Katastroficzne” to właściwe słowo. W skali od 1 do 10 jest to 11. ” Czytałem kilka lat temu, że jądro określonego systemu operacyjnego zostało rygorystycznie zweryfikowane za pomocą nowoczesnego systemu weryfikacji programów. Czy w ten sposób można …
3
Czy można udowodnić bezpieczeństwo wątków?
Biorąc pod uwagę program składający się ze zmiennych i instrukcji, które modyfikują te zmienne, oraz operację podstawową synchronizacji (monitor, mutex, Java zsynchronizowany lub blokada C #), czy można udowodnić, że taki program jest bezpieczny dla wątków? Czy istnieje nawet formalny model opisujący takie rzeczy, jak bezpieczeństwo wątków lub warunki wyścigowe?
Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.