> > Kupa różnych narzędzi weryfikuje adnotacje zaszyte w komentarzach. Statycznie. I
tak powinno być.
>
> Dlaczego? Bo właśnie do tego służą komentarze?

Powinno być statycznie.
Natomiast komentarze pozwalają "rozszerzyć" język bez ingerowania w kompilator.

> Jeżeli tak jest, to to wynika co najwyżej z tego, że macierzysty język jest zbyt
słaby, żeby wyrazić te rzeczy, które są istotne (i które weryfikują narzędzia, o
których mówisz). I dlatego używa się komentarzy jako takiego "haka" na wyrażanie tych
rzeczy.

Tak. Tak właśnie jest.
Język C jest słaby, więc używa się jego rozszerzeń w komentarzach, żeby wesprzeć jego
weryfikację. Zaletą takiego działania jest transparentność względem kompilatora.

> Słowo "asercja" można nawet znaleźć w Słowniku Języka Polskiego, jeśli komuś chce
się szukać.

Ale dryfujesz. Napisałem już kilka razy, dlaczego asercji się nie używa a Ty
grzebiesz w SJP, żeby... no właśnie nie wiem po co.

> możesz zdefiniować symbol NDEBUG przed załączeniem assert.h.

I w czym mi to pomoże?
Kod, który załaduję na produkcyjne urządzenie musi być *tym samym* kodem, który
przetestowałem, co do bitu. Nie ma opcji, żebym zrobił inaczej. Więc ten NDEBUG
musiałbym mieć zdefiniowany również w czasie testów.
To na cholerę mi takie asercje?

> Albo możesz np. zdefiniować
>
> #define certainly(x) do{}while(0)
>
> Wyjdzie w sumie na to samo.

Mógłbym. Ale po co miałbym definiować makro, któro nic nie robi?

> Asercje nie stanowią martwego kodu.

One są martwe z założenia. Nigdy się nie wykonują, więc są martwe.

> Standard C mówi wyłącznie, w jaki sposób jest zdefiniowane makro "assert".
> Nie mówi nic o tym, co oznacza słowo "asercja".

Dalej nie kumasz. Asercji nie używa się, bo stoją w konflikcie z innymi celami
procesów krytycznych. Twoje własne asercje też takie będą, nawet jeśli je będziesz
pisał na podstawie SJP.

> Dajmy na to, że mam taki komentarz:
>
> /* wartośc poniższego enuma służą jako indeksy do tablicy TABLICA */
>
> po którym następuje enum.
>
> I teraz, czy narzędzie sprawdzi mi, czy wartości tego enuma służą jako indeksy do
tablicy TABLICA?

Jeśli masz takie narzędzie, to sprawdzi.
Czego tu nie rozumiesz?

Przewiń sobie tą stronę i popatrz na komentarze w przykładach:

https://frama-c.com/acsl_tutorial_index.html

> Nie wiem, jakie standardy czytałeś, ale jeżeli idzie o te, z którymi ja miałem
styczność, to żadna nie rościła sobie pretensji do bycia normatywną w kwestii pojęcia
asercji.

Wniosek jest taki, że czytaliśmy różne standardy.

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