-
X-Received: by 2002:a37:6357:: with SMTP id x84mr143288qkb.4.1542882680799; Thu, 22
Nov 2018 02:31:20 -0800 (PST)
X-Received: by 2002:a37:6357:: with SMTP id x84mr143288qkb.4.1542882680799; Thu, 22
Nov 2018 02:31:20 -0800 (PST)
Path: news-archive.icm.edu.pl!news.icm.edu.pl!news.nask.pl!news.nask.org.pl!news.unit
0.net!weretis.net!feeder6.news.weretis.net!feeder.usenetexpress.com!feeder-in1.
iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!v55no26
03527qtk.0!news-out.google.com!m21ni4856qta.0!nntp.google.com!v55no2603524qtk.0
!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: pl.comp.programming
Date: Thu, 22 Nov 2018 02:31:20 -0800 (PST)
In-Reply-To: <a...@g...com>
Complaints-To: g...@g...com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=165.225.84.75;
posting-account=bMuEOQoAAACUUr_ghL3RBIi5neBZ5w_S
NNTP-Posting-Host: 165.225.84.75
References: <8...@g...com>
<7...@g...com>
<d...@g...com>
<psp6q7$97o$1@node2.news.atman.pl>
<6...@g...com>
<pss4d0$14n$1@node2.news.atman.pl>
<3...@g...com>
<8...@g...com>
<1...@g...com>
<8...@g...com>
<1...@g...com>
<a...@g...com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <9...@g...com>
Subject: Re: Niezmienniki pętli
From: Maciej Sobczak <s...@g...com>
Injection-Date: Thu, 22 Nov 2018 10:31:20 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Lines: 54
Xref: news-archive.icm.edu.pl pl.comp.programming:212970
[ ukryj nagłówki ]> Co masz na myśli mówiąc o pre- i post-conditions?
> Jaki język?
No właśnie dowolny i to jest ich zaletą, bo koncepcję można dokleić do dowolnego
języka, również do rzeczy, które niekoniecznie byśmy od razu skojarzyli z językiem
programowania, np. opis maszyny stanów.
https://en.wikipedia.org/wiki/Precondition
https://en.wikipedia.org/wiki/Postcondition
Tu jest kilka przykładów w SPARKu, zobacz gdzie są i jaką rolę pełnią słowa Pre i
Post w tych przykładach.
Da się to nawet dokleić do języka C, patrz np. Frama-C.
> > Mam wrażenie, że języki funkcjonalne za bardzo fiksują się na pojęciu typu. O ile
typ nadaje się do opisania dozwolonych stanów, to nie za bardzo nadaje się do
opisania przejść między stanami.
>
> To trochę takie pisanie palcem na piasku.
> Jak byś przedstawił konkretne przykłady, to może moglibyśmy
> spróbować podyskutować.
Przykład jest taki, że światło na skrzyżowaniu może być czerwone, żółte, zielone,
żółto-czerwone albo migające. To jest zbiór wartości, daje się to opisać typem
wyliczeniowym.
Da się też napisać funkcję zmieniającą stan świateł albo zwracającą kolejny stan w
sekwencji, itp. Wiem, jak ładnie napisać system obsługujący np. szlaban na
przejeździe kolejowym przy użyciu takich pojęć jak pre- i post-conditions, po te
pojęcia nadają się do pracy z systemami, w których np. coś ma być spełnione żeby coś
mogło być po czymś. Tu pojęcia "przed" i "po" pojawiają się naturalnie i podobnie
jest w każdym innym systemie, dającym się opisać maszyną stanów (pralka, zmywarka,
skrzynia biegów, samolot, itd.).
Widziałem kilka teoretycznych przykładów z dependent types, ale żadnego praktycznego,
który mógłby pomóc w takich właśnie stanowo-sekwencyjnych systemach. A łaśnie takie
są w systemach krytycznych, bo przypadkiem ich krytyczność wynika z tego, że są
związane z procesami fizycznymi, w których jest czas a jak jest czas, to jest też
"pre" i "post".
Właśnie dlatego wsparcie dla "pre" i "post" w języku programowania jest czymś bardzo
cennym. Pytanie, czy dependent types cokolwiek tu jeszcze wnoszą, czego nie da się
pokryć samym "pre" i "post".
--
Maciej Sobczak * http://www.inspirel.com
Następne wpisy z tego wątku
- 22.11.18 15:22 fir
- 22.11.18 16:08 AK
- 22.11.18 18:50 Sebastian Biały
- 22.11.18 18:53 Sebastian Biały
- 22.11.18 22:53 Wojciech Muła
- 22.11.18 23:25 AK
- 23.11.18 00:41 AK
- 23.11.18 00:43 AK
- 23.11.18 07:33 s...@g...com
- 23.11.18 08:00 Wojciech Muła
- 23.11.18 10:34 AK
- 23.11.18 10:38 AK
- 23.11.18 13:08 Wojciech Muła
- 23.11.18 13:10 Wojciech Muła
- 23.11.18 14:46 Maciej Sobczak
Najnowsze wątki z tej grupy
- Nowa ustawa o ochronie praw autorskich - opis problemu i szkic ustawy
- Alg. kompresji LZW
- Popr. 14. Nauka i Praca Programisty C++ w III Rzeczy (pospolitej)
- Arch. Prog. Nieuprzywilejowanych w pełnej wer. na nowej s. WWW energokod.pl
- 7. Raport Totaliztyczny: Sprawa Qt Group wer. 424
- TCL - problem z escape ostatniego \ w nawiasach {}
- Nauka i Praca Programisty C++ w III Rzeczy (pospolitej)
- testy-wyd-sort - Podsumowanie
- Tworzenie Programów Nieuprzywilejowanych Opartych Na Wtyczkach
- 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
Najnowsze wątki
- 2025-03-19 Brak ograniczeń dla chińskiego kapitału - wam nie do rządu, tylko na zmywak do chińskiej knajpy!!!
- 2025-03-19 Wietnam wykłada 500M$ i chce zbudować fabrykę za 50G$
- 2025-03-19 szal-Unia == federacja policyjna
- 2025-03-19 Polsza == państwo policyjne
- 2025-03-19 Grzegorz Płaczek o programie szczepień dzieci. ,,Stworzono eldorado dla firm farmaceutycznych"
- 2025-03-19 Wietnam wykłada 500M$ i chce zbudować fabrykę za 50G$
- 2025-03-19 Gemini
- 2025-03-19 Mokry sen Zenka :)
- 2025-03-19 Re: Dlaczego tak odstają od Tesli?
- 2025-03-19 Czy grupa p.s.prawo przetrwa najbliższe wybory (prezydenta)?
- 2025-03-19 Warszawa => Frontend Developer (obszar Angular13+) <=
- 2025-03-19 Czy "niedopuszczony pełnomocnik" jest w prawie się na to skarżyć jak "świadek" zmarła bez zostawienia mu takiej instrukcji?
- 2025-03-19 Kraków => Business Development Manager - Network and Network Security
- 2025-03-19 Ostrów Świętokrzy => Node.js / Fullstack Developer <=
- 2025-03-19 Kraków => IT Expert (Network Systems area) <=