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