🚀 go-pugleaf

RetroBBS NetNews Server

Inspired by RockSolid Light RIP Retro Guy

Article View: pl.comp.programming
Article #215976

Re: Jak to robią w NASA

#215976
From: godek.maciek
Date: Fri, 06 Sep 2019 21:00
77 lines
6001 bytes
W dniu piątek, 6 września 2019 21:25:18 UTC+2 użytkownik Maciej Sobczak napisał:
> > > 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.

Dla ścisłości, formalne wyrażenia zaszyte w komentarzach.
Czyli drugi 'język programowania'. Tylko pewnie z gorszym wsparciem narzędzi.

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

No bo błędnie napisałeś.

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

Bo po pierwsze, możesz je inaczej interpretować poza swoim procesem.
Po drugie, możesz pewne rzeczy wyrazić w tym samym języku, w którym piszesz program. Po trzecie, na cholerę Ci komentarze? Po czwarte, tak jak masz narzędzia, które parsują formalny język w komentarzach, to mogłyby też tak samo parsować i statycznie weryfikować asercje - bo czemu nie?

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

Po co pisać komentarz, który 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.

Nie mam takiego narzędzia.

> Czego tu nie rozumiesz?

Nie rozumiem w jaki sposób magiczne narzędzia mają nagle czytać moje komentarze ze zrozumieniem. W komentarzach mogę pisać cokolwiek. Jak narzędzie mi sprawdzi, że nie kłamię?

> Przewiń sobie tą stronę i popatrz na komentarze w przykładach:
> 
> https://frama-c.com/acsl_tutorial_index.html

No to wygląda mi na takie rzeczy, które mogę wyrazić w asercjach.

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

No to dajesz cytaty.
Technical Details
Message-ID: <8c636dbb-1628-4476-88cd-4578d874ae98@googlegroups.com>
Path: mbox-mo1.pugleaf.net!news-archive.icm.edu.pl!news.icm.edu.pl!newsfeed.pionier.net.pl!news-1.dfn.de!news.dfn.de!news.uni-stuttgart.de!news.unit0.net!newsreader4.netcologne.de!news.netcologne.de!peer01.ams1!peer.ams1.xlned.com!news.xlned.com!peer01.am4!peer.am4.highwinds-media.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!o24no6253868qtl.0!news-out.google.com!d29ni892qtg.1!nntp.google.com!o24no6253854qtl.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
References: <1ua4wui506zbf$.dlg@tyczka.com> <qkecqc$c03$1@news.icm.edu.pl> <3ec85b36-33be-49bd-b688-d8c9213a771a@googlegroups.com> <qkicu0$knb$1@gioia.aioe.org> <46e56026-21be-4761-908e-7991c72a1143@googlegroups.com> <qkjqqi$1b59$1@gioia.aioe.org> <0125b7f3-d337-4537-a6d3-237b78065215@googlegroups.com> <rmvauunflug0.dlg@tyczka.com> <eab71553-8760-428b-a4aa-a58ac0f346ec@googlegroups.com> <1794fcdb-d7bb-402f-927f-80010b217989@googlegroups.com> <1a2f7fe3-5745-40b2-9fd6-868fca99dea5@googlegroups.com> <a0c6a1c7-e8bf-4079-b5f2-d5dcec42f7d9@googlegroups.com> <819e71ad-be91-42ae-a41a-76628f10bcbf@googlegroups.com> <4ecd1b3c-579b-4660-896f-76d8ed9298c6@googlegroups.com> <eb02743f-41b4-4dd0-862b-a21d6b96729f@googlegroups.com>

Show Full Headers
Complete Article Headers
X-Received: by 2002:a0c:e74b:: with SMTP id g11mr1565179qvn.62.1567803604691;        Fri, 06 Sep 2019 14:00:04 -0700 (PDT)
X-Received: by 2002:a0c:ca02:: with SMTP id c2mr7028737qvk.209.1567803604445; Fri, 06 Sep 2019 14:00:04 -0700 (PDT)
Path: mbox-mo1.pugleaf.net!news-archive.icm.edu.pl!news.icm.edu.pl!newsfeed.pionier.net.pl!news-1.dfn.de!news.dfn.de!news.uni-stuttgart.de!news.unit0.net!newsreader4.netcologne.de!news.netcologne.de!peer01.ams1!peer.ams1.xlned.com!news.xlned.com!peer01.am4!peer.am4.highwinds-media.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!o24no6253868qtl.0!news-out.google.com!d29ni892qtg.1!nntp.google.com!o24no6253854qtl.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: pl.comp.programming
Date: Fri, 6 Sep 2019 14:00:04 -0700 (PDT)
In-Reply-To: <eb02743f-41b4-4dd0-862b-a21d6b96729f@googlegroups.com>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=83.25.253.100; posting-account=f7iIKQoAAAAkDKpUafc-4IXhmRAzdB5r
NNTP-Posting-Host: 83.25.253.100
References: <1ua4wui506zbf$.dlg@tyczka.com> <qkecqc$c03$1@news.icm.edu.pl> <3ec85b36-33be-49bd-b688-d8c9213a771a@googlegroups.com> <qkicu0$knb$1@gioia.aioe.org> <46e56026-21be-4761-908e-7991c72a1143@googlegroups.com> <qkjqqi$1b59$1@gioia.aioe.org> <0125b7f3-d337-4537-a6d3-237b78065215@googlegroups.com> <rmvauunflug0.dlg@tyczka.com> <eab71553-8760-428b-a4aa-a58ac0f346ec@googlegroups.com> <1794fcdb-d7bb-402f-927f-80010b217989@googlegroups.com> <1a2f7fe3-5745-40b2-9fd6-868fca99dea5@googlegroups.com> <a0c6a1c7-e8bf-4079-b5f2-d5dcec42f7d9@googlegroups.com> <819e71ad-be91-42ae-a41a-76628f10bcbf@googlegroups.com> <4ecd1b3c-579b-4660-896f-76d8ed9298c6@googlegroups.com> <eb02743f-41b4-4dd0-862b-a21d6b96729f@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <8c636dbb-1628-4476-88cd-4578d874ae98@googlegroups.com>
Subject: Re: Jak to robią w NASA
From: godek.maciek@gmail.com
Injection-Date: Fri, 06 Sep 2019 21:00:04 +0000
X-Received-Bytes: 6767
X-Received-Body-CRC: 4129047877
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit