Użytkownik <j...@p...onet.pl> napisał:

Zdaje się, że pierwszym niepoważnym w tym wątku jesteś Ty sam. I dlatego
otrzymujesz niepoważne w Twoim mniemaniu odpowiedzi. Co to znaczy
"poprawność programu"? Sprecyzuj.

Jeśli dobrze się domyslam o co Ci chodzi to:

- właśnie testy są podstawą
- test testowi nierówny
- są różne metody i sposoby

Poważne firmy do testowania swoich programów stosują rozbudowane metody i
specjalne programy, które sprawdzaja program pod kątem:

- czy nie zawiesza się, lub systemu w trakcie długiego działania
- czy nie spowalnia pracy i nie zzera pamięci
- czy podaje prawidłowe wyniki w zależności od danych wejściowych
- reakcję na różne, w tym możliwe nieprawidłowe dane wejściowe

To tylko drobna cząstka tego co jest badane i chodzi o zrozumienie w czym
rzecz.

I ostatnia uwaga. Nigdy do końca nie wiadomo, czy program nie zawiera
błedów.

Remek

do góry

On 11 Sie, 21:35, "Remek" <b...@t...pl> wrote:

> - czy nie zawiesza się, lub systemu w trakcie długiego działania
> - czy nie spowalnia pracy i nie zzera pamięci
> - czy podaje prawidłowe wyniki w zależności od danych wejściowych
> - reakcję na różne, w tym możliwe nieprawidłowe dane wejściowe
>
> To tylko drobna cząstka tego co jest badane i chodzi o zrozumienie w czym
> rzecz.
Czasami używam metody "wielu różnych algorytmów do tego samego
problemu" - wszystkie powinny dać taki sam wynik. Struktura danych
jest przetasowana, algorytm inny, więc przy 3 różnych algorytmach i
wielu różnorodnych danych wejściowych prawdopodobieństwo błędu
szybko spada do zera.

Pozdrawiam

do góry

> to wcale nie była niepoważna odpowiedź.

Przez przypatrzenie to można sobie udowodnić poprawność programu Hello World.
Przez zaliczenie można zaliczyć niepoprawny program u niekompetentnego prowadzącego.
Przez dochód - można zrobić majątek na pełnym bugów Windows.


--
Wysłano z serwisu OnetNiusy: http://niusy.onet.pl

do góry

j...@p...onet.pl wrote:

>> to wcale nie była niepoważna odpowiedź.
>
> Przez przypatrzenie to można sobie udowodnić poprawność programu Hello
> World. Przez zaliczenie można zaliczyć niepoprawny program u
> niekompetentnego prowadzącego. Przez dochód - można zrobić majątek na
> pełnym bugów Windows.

Wszystko to prawda.
Ilustruje ona tylko fakt, ze definicja slowa "poprawnosc" zalezy od tego,
kto i po co ja formuluje. Zas od tejze definicji zaleza metody weryfikacji
poprawnosci.

Czyli:
dla studenta - program "poprawny" == "zaliczony"
dla firmy - program "poprawny" == "przynoszacy (duze) zyski"
dla hobbysty - program "poprawny" == "jestem z niego (na oko) zadowolony"

--
Michal

do góry

> Co to znaczy "poprawność programu"? Sprecyzuj.

Każdy student informatyki wie, że:
poprawność = częściowa poprawność + własność stopu + określoność obliczeń
gdzie częsciowa poprawność = zgodność z formalną specyfikacją

> Nigdy do końca nie wiadomo, czy program nie zawiera błedów.

No właśnie o to chodzi, że testami się tej pewności nie osiągnie, natomiast są
metody formalne, np. logika Hoare'a które taką pewność dają. Problem, w tym, że
są to metody pracochłonne i - przy bardziej skomplikowanych programach - trudne
matematycznie. Stąd całe moje pytanie: czy programiści wykorzystują je w
praktyce. Oczywiście są sytuacje kiedy dowód formalny poprawności jest bardzo
pożądany, np. gdy od poprawności programu zależy ludzkie życie.


--
Wysłano z serwisu OnetNiusy: http://niusy.onet.pl

do góry

j...@p...onet.pl wrote:

>> Co to znaczy "poprawność programu"? Sprecyzuj.
>
> Każdy student informatyki wie, że:
> poprawność = częściowa poprawność + własność stopu + określoność obliczeń
> gdzie częsciowa poprawność = zgodność z formalną specyfikacją
>

Wlasnie. W praktyce taki byt jak "formalna specyfikacja" wystepuje baaardzo
rzadko. Co wiecej - nawet jesli wystepuje, to dowiedzenie zgodnosci z
formalna specyfikacja nie dowodzi poprawnosci programu zdefiniowanej jako
"klient/uzytkownik/sponsor ma byc zadowolony". Zeby to osiagnac trzeba
operowac na "metapoziomie" czyli wdrozyc jakis system zapewnienia jakosci.

--
Michal

do góry

> system zapewnienia jakosci.

O to mi właśnie chodziło. Dzięki za odpowiedź.


--
Wysłano z serwisu OnetNiusy: http://niusy.onet.pl

do góry

On 17 Sie, 13:01, j...@p...onet.pl wrote:

> Każdy student informatyki wie, że:
> poprawność = częściowa poprawność + własność stopu + określoność obliczeń
> gdzie częsciowa poprawność = zgodność z formalną specyfikacją

To zależy, gdzie student studiował.

http://en.wikipedia.org/wiki/Partial_correctness

Częściowa poprawność oznacza, że JEŚLI program w ogóle da jakieś
wyniki, to będą one poprawne. W szczególności częściowa poprawność nie
chroni przed zapętleniem się.

> No właśnie o to chodzi, że testami się tej pewności nie osiągnie, natomiast są
> metody formalne, np. logika Hoare'a które taką pewność dają. Problem, w tym, że
> są to metody pracochłonne i - przy bardziej skomplikowanych programach - trudne
> matematycznie. Stąd całe moje pytanie: czy programiści wykorzystują je w
> praktyce.

Tak. Jednym z ciekawszych rozwiązań w tym zakresie jest SPARK:

http://en.wikipedia.org/wiki/SPARK

Jest ciekawy dlatego, że będąc podzbiorem znanego już języka
imperatywnego jest też od razu kompilowalny do kodu wynikowego. To nie
są jakieś obrazki czy inne matematyczne robaczki, tylko żywy kod z
dodatkową specyfikacją nt. przepływu informacji czy pre/post-
conditions. Weryfikuje się taki kod odpowiednimi narzędziami a potem
wrzuca do normalnego kompilatora i działa. Sporo tym można zrobić i
nawet się tego używa w praktyce a ponieważ kompletny zbiór narzędzi
jest dostępny za friko, to jest to też dobra platforma dla samouków.

> Oczywiście są sytuacje kiedy dowód formalny poprawności jest bardzo
> pożądany, np. gdy od poprawności programu zależy ludzkie życie.

Nadal pozostaje pytanie o poprawność specyfikacji. Można spokojnie
udowodnić poprawność źle wyspecyfikowanego programu - program będzie
idealnie robił nie to, co trzeba. Niestety zawsze gdzieś będzie
miejsce na czynnik ludzki jako najsłabsze ogniwo.

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

do góry

> Poza tym dobrze zrobione testy są wystarczające.
A co gdy nie jesteś pewien czy trudniejszy algorytm jest poprawny a zbiór
możliwych danych wejściowych obszerny? Będziesz go testował i możesz nigdy nie
trafić na dane wejściowe, przy których źle działa.

> Czegoś trudniejszego od "hallo world" nie jesteś w stanie dowieść.
Udało mi się kiedyś.


--
Wysłano z serwisu OnetNiusy: http://niusy.onet.pl

do góry

> Tak. Jednym z ciekawszych rozwiązań w tym zakresie jest SPARK

Nie znam SPARKa.
Czy wstawianie asercji ma sens tzn. coś pomaga?

function assert($condition, $message = null) {
if (!$condition) {
echo (!empty($message) ? $message : 'Błąd wewnętrzny.');
exit;
}
}

--
Wysłano z serwisu OnetNiusy: http://niusy.onet.pl

do góry