🚀 go-pugleaf

> > 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