-
X-Received: by 2002:a0c:b999:: with SMTP id v25mr11600383qvf.80.1567973839566; 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: news-archive.icm.edu.pl!news.icm.edu.pl!newsfeed.pionier.net.pl!3.eu.feeder.erj
e.net!feeder.erje.net!feeder1.usenet.farm!feed.usenet.farm!newsfeed.xs4all.nl!n
ewsfeed7.news.xs4all.nl!85.12.16.69.MISMATCH!peer02.ams1!peer.ams1.xlned.com!ne
ws.xlned.com!peer02.am4!peer.am4.highwinds-media.com!peer03.iad!feed-me.highwin
ds-media.com!news.highwinds-media.com!o24no965097qtl.0!news-out.google.com!d29n
i1190qtg.1!nntp.google.com!o24no965091qtl.0!postnews.google.com!glegroupsg2000g
oo.googlegroups.com!not-for-mail
Newsgroups: pl.comp.programming
Date: Sun, 8 Sep 2019 13:17:19 -0700 (PDT)
In-Reply-To: <6...@g...com>
Complaints-To: g...@g...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>
<3...@g...com>
<qkicu0$knb$1@gioia.aioe.org>
<4...@g...com>
<qkjqqi$1b59$1@gioia.aioe.org>
<0...@g...com>
<r...@t...com>
<e...@g...com>
<1...@g...com>
<1...@g...com>
<a...@g...com>
<8...@g...com>
<4...@g...com>
<e...@g...com>
<8...@g...com>
<f...@g...com>
<6...@g...com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <e...@g...com>
Subject: Re: Jak to robią w NASA
From: Maciej Sobczak <s...@g...com>
Injection-Date: Sun, 08 Sep 2019 20:17:19 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Received-Bytes: 3788
X-Received-Body-CRC: 1402183938
Xref: news-archive.icm.edu.pl pl.comp.programming:213980
[ ukryj nagłówki ]> 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
Następne wpisy z tego wątku
- 09.09.19 17:56 AK
- 11.09.19 07:30 M.M.
- 11.09.19 09:21 Maciej Sobczak
- 11.09.19 20:09 AK
- 11.09.19 20:32 M.M.
- 12.09.19 09:21 Maciej Sobczak
- 12.09.19 12:05 M.M.
- 13.09.19 08:14 Maciej Sobczak
Najnowsze wątki z tej grupy
- Do czego nadaje się QDockWidget z bibl. Qt?
- Bibl. Qt jest sztucznie ograniczona - jest nieprzydatna do celów komercyjnych
- Co sciaga kretynow
- AEiC 2024 - Ada-Europe conference - Deadlines Approaching
- Jakie są dobre zasady programowania programów opartych na wtyczkach?
- sprawdzanie słów kluczowych dot. zła
- Re: W czym sie teraz pisze programy??
- Re: (PDF) Surgical Pathology of Non-neoplastic Gastrointestinal Diseases by Lizhi Zhang
- CfC 28th Ada-Europe Int. Conf. Reliable Software Technologies
- Młodzi programiści i tajna policja
- Ada 2022 Language Reference Manual to be Published by Springer
- Press Release - AEiC 2023, Ada-Europe Reliable Softw. Technol.
- Ada-Europe - AEiC 2023 early registration deadline approaching
- Ada-Europe Int.Conf. Reliable Software Technologies, AEiC 2023
- Ile cykli zajmuje mnożenie liczb 64-bitowych?
Najnowsze wątki
- 2024-05-18 Warszawa => Software .Net Developer <=
- 2024-05-18 Warszawa => Mid/Senior QA Engineer <=
- 2024-05-18 Ulm => Solution Architect (sichere Kommunikation und IoT-Loesungen <=
- 2024-05-18 Katowice => Head of Virtualization Platform Management and Operating S
- 2024-05-18 Warszawa => SAP WM Consultant / Execution <=
- 2024-05-18 Wrocław => Consultant/Implementer Comarch ERP XL <=
- 2024-05-18 Gdańsk => Head of International Freight Forwarding Department <=
- 2024-05-18 Warszawa => Account Manager (Recruitment Services) <=
- 2024-05-18 Łódź => Salesperson - CRM Systems <=
- 2024-05-18 Łódź => Handlowiec - Systemy CRM <=
- 2024-05-17 ZŁOMNIK o pracy w TVN TURBO, nowych przepisach i współczesnej motoryzacji. Turbo Taryfa!
- 2024-05-17 Białystok => DevOps Engineer Conexa First (Contractor) <=
- 2024-05-17 Warszawa => Starszy inżynier oprogramowania (Rust) <=
- 2024-05-17 Zabrze => Junior HelpDesk <=
- 2024-05-17 Bieruń => Administrator i wdrożeniowiec Lotus Notes/Domino <=