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

> Nie znam SPARKa.

Polecam, bo w przeciwieństwie do wielu akademickich pomysłów ten język
wydaje się nawet rozwijać.

> Czy wstawianie asercji ma sens tzn. coś pomaga?

Asercje w SPARKu są sprawdzane statycznie (jak wszystko inne) i
pomagają w tym sensie, że dają narzędziom dodatkowe informacje nt.
tego, co programista myśli o swoim kodzie.
W szczególności asercje w SPARKu są potrzebne do tego, żeby przeciąć
pętle poprzez ustalenie ich niezmienników - to pozwala na sensowną
analizę tych pętli.
Asercje istnieją jednak tylko w czasie kompilacji, bo potem są już
niepotrzebne.

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

To wygląda na konstrukcję run-time, czyli nie ma związku ze
statyczną weryfikacją czegokolwiek. W językach z pełną statyczną
analizą asercje run-time kompletnie nic nie dają - bo skoro analiza
była statyczna, to wiadomo z góry, że asercja zawsze się sprawdzi i
wtedy można ją po prostu wyeliminować z kodu. Dokładnie na tej
zasadzie SPARK eliminuje potrzebę sprawdzania np. indeksów w
tablicach, dzielenia przez zero, itd. - skoro z analizy wiadomo, że
takich rzeczy w programie nie ma, to nie trzeba generować kodu, który
to sprawdza albo który na to reaguje.

Asercje run-time mają jednak sens w tych językach, które nie są zdolne
do pełnej analizy statycznej i mogą służyć do wykrywania kompletnych
fakapów w czasie wykonania programu. Znajdziesz je poutykane w kodzie
w Javie, w C++, itd.

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

do góry

On Tue, 17 Aug 2010, Maciej Sobczak wrote:

>
> http://en.wikipedia.org/wiki/Partial_correctness
>
> Czesciowa poprawnosc oznacza, ze JESLI program w ogole da jakies
> wyniki, to beda one poprawne. W szczegolnosci czesciowa poprawnosc nie
> chroni przed zapetleniem sie.

ale program zapetlony nigdy nie zwroci wyniku, z czego wynika ze nie moze
byc poprawny

do góry

Na początku tej dyskusji wkradł się błąd, który propaguje :-)
Otóż o poprawności (ang correctness) (jako o terminie w naukach
komputerowych) mówimy odnosząc się do algorytmów .
W odniesieniu do programów, tzn. implementacji tych algorytmów, tzn.
kodu, mówi się o JAKOŚCI (ang. quality).

do góry

On 18 Sie, 08:36, shio <s...@b...eu.org> wrote:

> > Czesciowa poprawnosc oznacza, ze JESLI program w ogole da jakies
> > wyniki, to beda one poprawne. W szczegolnosci czesciowa poprawnosc nie
> > chroni przed zapetleniem sie.
>
> ale program zapetlony nigdy nie zwroci wyniku, z czego wynika ze nie moze
> byc poprawny

Skoro nigdy nie zwróci wyniku, to znaczy, że nigdy nie zwróci błędnego
wyniku. To bardzo dobry program. :-)

Właśnie dlatego mówimy o poprawności *częściowej*.
Chodzi tutaj też o ograniczenia narzędzi weryfikujących. Poprawność
częściową można udowadniać automatycznie metodami, które mają jeszcze
sensowną złożoność obliczeniową i dają się stosować (tzn. skalować) w
praktyce.

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

do góry

On Wed, 18 Aug 2010, Maciej Sobczak wrote:

>>> Czesciowa poprawnosc oznacza, ze JESLI program w ogole da jakies
>>> wyniki, to beda one poprawne. W szczegolnosci czesciowa poprawnosc nie
>>> chroni przed zapetleniem sie.
>>
>> ale program zapetlony nigdy nie zwroci wyniku, z czego wynika ze nie moze
>> byc poprawny
>
> Skoro nigdy nie zwroci wyniku, to znaczy, ze nigdy nie zwroci blednego
> wyniku. To bardzo dobry program. :-)

Moze i bardzo dobry ale niepoprawny:-) skoro czesciowa poprawnosc ma
oznaczac, ze W OGOLE zwraca jakis wynik. Program zapetlony nie zwroci. Juz
w tym watku zwrocono juz uwage na pomieszanie pojec algorytmu, co do
ktorego mozna mowic o poprawnosci, z jego implementacja. Niemniej mysle
jednak, ze to ma sens - czesciowa poprawnosc implementacji oznaczalaby, ze program
zwroci wynik, ktory moze
byc niezgodny do konca z wymaganiem funkcjonalnym ale nie bedzie to np.
wyjatek. Musze przyznac, ze czesto mam do czynienia z tak rozumianymi
czesciowo poprawnymi programami:)

do góry