Re: Jak to robią w NASA

Article View: pl.comp.programming

Article #215980

Back to pl.comp.programming Previous Next

#215980

From: Maciej Sobczak
Date: Sun, 08 Sep 2019 20:17

28 lines
3730 bytes

> No to spróbujmy pierwszy przykład:
> 
> /*@ ensures \result >= x && \result >= y; 
>     ensures \result == x || \result == y; 
> */ 
> int max (int x, int y) { return (x > y) ? x : y; } 
> 
> int max (int x, int y) {
>   int result = (x > y) ? x : y;
>   assert(result >= x && result >= y);
>   assert(result == x || result == y);
>   return result;
> }
> 
> Udało się.

Nie udało się, z czterech powodów.

Po pierwsze, asercje (nazwijmy je raczej warunkami weryfikacji) w tych przykładach są właściwością deklaracji funkcji a nie jej ciała. Oznacza to, że są użyteczne zarówno przy weryfikacji ciała funkcji jak i przy weryfikacji kodu wołającego. Twoje asserty w ciele pełnią tylko tą pierwszą rolę, co je bardzo ogranicza.

Po drugie, warunki w komentarzach, gdzie są analizowane przez zewnętrzne narzędzie, nie podlegają ograniczeniom języka C i mogą korzystać nie tylko z szerszej składni, ale w ogóle z innego paradygmatu.

Po trzecie, na tym *pierwszym* przykładzie kończą się Twoje możliwości w tym zakresie. Niezbyt imponująco. Dalsze przykłady są ciekawsze (co nawiązuje do poprzedniego punktu).

Po czwarte wreszcie, Twoja wersja ma dead code. Mam nadzieję, że to nie wymaga ponownego wyjaśnienia.

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

Technical Details

Message-ID: <efda217d-c77f-474c-9528-f27c49f9bf99@googlegroups.com>

Path:

mbox-mo1.pugleaf.net!news-archive.icm.edu.pl!news.icm.edu.pl!newsfeed.pionier.net.pl!3.eu.feeder.erje.net!feeder.erje.net!feeder1.usenet.farm!feed.usenet.farm!newsfeed.xs4all.nl!newsfeed7.news.xs4all.nl!85.12.16.69.MISMATCH!peer02.ams1!peer.ams1.xlned.com!news.xlned.com!peer02.am4!peer.am4.highwinds-media.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!o24no965097qtl.0!news-out.google.com!d29ni1190qtg.1!nntp.google.com!o24no965091qtl.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> <8c636dbb-1628-4476-88cd-4578d874ae98@googlegroups.com> <fa84e279-9339-4ef2-84b4-4ed0058163e2@googlegroups.com> <6ca46f89-2f05-450e-8a97-e05f4c5968f1@googlegroups.com>

Show Full Headers

Complete Article Headers

X-Received: by 2002:a37:9303:: with SMTP id v3mr20346020qkd.369.1567973839839;        Sun, 08 Sep 2019 13:17:19 -0700 (PDT)
X-Received: by 2002:a0c:b999:: with SMTP id v25mr11600383qvf.80.1567973839566; Sun, 08 Sep 2019 13:17:19 -0700 (PDT)
Path: mbox-mo1.pugleaf.net!news-archive.icm.edu.pl!news.icm.edu.pl!newsfeed.pionier.net.pl!3.eu.feeder.erje.net!feeder.erje.net!feeder1.usenet.farm!feed.usenet.farm!newsfeed.xs4all.nl!newsfeed7.news.xs4all.nl!85.12.16.69.MISMATCH!peer02.ams1!peer.ams1.xlned.com!news.xlned.com!peer02.am4!peer.am4.highwinds-media.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!o24no965097qtl.0!news-out.google.com!d29ni1190qtg.1!nntp.google.com!o24no965091qtl.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: pl.comp.programming
Date: Sun, 8 Sep 2019 13:17:19 -0700 (PDT)
In-Reply-To: <6ca46f89-2f05-450e-8a97-e05f4c5968f1@googlegroups.com>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=213.108.152.51; posting-account=bMuEOQoAAACUUr_ghL3RBIi5neBZ5w_S
NNTP-Posting-Host: 213.108.152.51
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> <8c636dbb-1628-4476-88cd-4578d874ae98@googlegroups.com> <fa84e279-9339-4ef2-84b4-4ed0058163e2@googlegroups.com> <6ca46f89-2f05-450e-8a97-e05f4c5968f1@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <efda217d-c77f-474c-9528-f27c49f9bf99@googlegroups.com>
Subject: Re: Jak to robią w NASA
From: Maciej Sobczak <see.my.homepage@gmail.com>
Injection-Date: Sun, 08 Sep 2019 20:17:19 +0000
X-Received-Bytes: 3788
X-Received-Body-CRC: 1402183938
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Reply to Parent Message