Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > pl.comp.programming > #31990 > unrolled thread
| Started by | Maciej Sobczak <see.my.homepage@gmail.com> |
|---|---|
| First post | 2018-11-16 00:27 -0800 |
| Last post | 2018-11-29 00:08 -0800 |
| Articles | 11 on this page of 91 — 10 participants |
Back to article view | Back to pl.comp.programming
Niezmienniki pętli Maciej Sobczak <see.my.homepage@gmail.com> - 2018-11-16 00:27 -0800
Re: Niezmienniki pętli queequeg@trust.no1 (Queequeg) - 2018-11-16 15:22 +0000
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-16 17:18 +0100
Re: Niezmienniki pętli szykcech@gmail.com - 2018-11-16 07:48 -0800
Re: Niezmienniki pętli szykcech@gmail.com - 2018-11-16 07:50 -0800
Re: Niezmienniki pętli queequeg@trust.no1 (Queequeg) - 2018-11-16 19:14 +0000
Re: Niezmienniki pętli szykcech@gmail.com - 2018-11-16 11:40 -0800
Re: Niezmienniki pętli queequeg@trust.no1 (Queequeg) - 2018-11-16 20:05 +0000
Re: Niezmienniki pętli szykcech@gmail.com - 2018-11-17 07:59 -0800
Re: Niezmienniki pętli queequeg@trust.no1 (Queequeg) - 2018-11-18 00:02 +0000
Re: Niezmienniki pętli Maciej Sobczak <see.my.homepage@gmail.com> - 2018-11-16 14:51 -0800
Re: Niezmienniki pętli queequeg@trust.no1 (Queequeg) - 2018-11-19 09:37 +0000
Re: Niezmienniki pętli fir <profesor.fir@gmail.com> - 2018-11-18 01:10 -0800
Re: Niezmienniki pętli fir <profesor.fir@gmail.com> - 2018-11-18 01:28 -0800
Re: Niezmienniki pętli godek.maciek@gmail.com - 2018-11-16 11:51 -0800
Re: Niezmienniki pętli Maciej Sobczak <see.my.homepage@gmail.com> - 2018-11-16 14:55 -0800
Re: Niezmienniki pętli Sebastian Biały <heby@poczta.onet.pl> - 2018-11-17 14:58 +0100
Re: Niezmienniki pętli Maciej Sobczak <see.my.homepage@gmail.com> - 2018-11-17 15:10 -0800
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-18 09:58 +0100
Re: Niezmienniki pętli Sebastian Biały <heby@poczta.onet.pl> - 2018-11-18 17:35 +0100
Re: Niezmienniki pętli Maciej Sobczak <see.my.homepage@gmail.com> - 2018-11-18 23:14 -0800
Re: Niezmienniki pętli Roman Tyczka <noemail@because.no> - 2018-11-19 09:22 +0100
Re: Niezmienniki pętli godek.maciek@gmail.com - 2018-11-19 08:15 -0800
Re: Niezmienniki pętli godek.maciek@gmail.com - 2018-11-19 10:45 -0800
Re: Niezmienniki pętli Sebastian Biały <heby@poczta.onet.pl> - 2018-11-22 18:50 +0100
Re: Niezmienniki pętli godek.maciek@gmail.com - 2018-11-19 10:49 -0800
Re: Niezmienniki pętli szykcech@gmail.com - 2018-11-19 12:18 -0800
Re: Niezmienniki pętli queequeg@trust.no1 (Queequeg) - 2018-11-19 20:44 +0000
Re: Niezmienniki pętli fir <profesor.fir@gmail.com> - 2018-11-19 13:10 -0800
Re: Niezmienniki pętli fir <profesor.fir@gmail.com> - 2018-11-19 13:16 -0800
Re: Niezmienniki pętli queequeg@trust.no1 (Queequeg) - 2018-11-20 09:43 +0000
Re: Niezmienniki pętli fir <profesor.fir@gmail.com> - 2018-11-20 01:58 -0800
Re: Niezmienniki pętli godek.maciek@gmail.com - 2018-11-20 14:27 -0800
Re: Niezmienniki pętli queequeg@trust.no1 (Queequeg) - 2018-11-21 10:12 +0000
Re: Niezmienniki pętli godek.maciek@gmail.com - 2018-11-21 11:35 -0800
Re: Niezmienniki pętli queequeg@trust.no1 (Queequeg) - 2018-11-21 21:10 +0000
Re: Niezmienniki pętli fir <profesor.fir@gmail.com> - 2018-11-21 02:36 -0800
Re: Niezmienniki pętli godek.maciek@gmail.com - 2018-11-19 14:12 -0800
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-20 00:20 +0100
Re: Niezmienniki pętli queequeg@trust.no1 (Queequeg) - 2018-11-20 09:35 +0000
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-20 12:00 +0100
Re: Niezmienniki pętli szykcech@gmail.com - 2018-11-19 20:37 -0800
Re: Niezmienniki pętli godek.maciek@gmail.com - 2018-11-20 13:46 -0800
Re: Niezmienniki pętli fir <profesor.fir@gmail.com> - 2018-11-20 01:46 -0800
Re: Niezmienniki pętli fir <profesor.fir@gmail.com> - 2018-11-20 12:52 -0800
Re: Niezmienniki pętli fir <profesor.fir@gmail.com> - 2018-11-20 13:16 -0800
Re: Niezmienniki pętli Maciej Sobczak <see.my.homepage@gmail.com> - 2018-11-20 06:07 -0800
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-20 17:54 +0100
Re: Niezmienniki pętli Maciej Sobczak <see.my.homepage@gmail.com> - 2018-11-20 23:16 -0800
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-21 15:54 +0100
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-21 16:07 +0100
Re: Niezmienniki pętli Maciej Sobczak <see.my.homepage@gmail.com> - 2018-11-21 13:48 -0800
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-22 16:08 +0100
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-20 00:00 +0100
Re: Niezmienniki pętli Wojciech Muła <wojtek.mula@gmail.com> - 2018-11-22 13:53 -0800
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-22 23:25 +0100
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-23 00:41 +0100
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-23 00:43 +0100
Re: Niezmienniki pętli szykcech@gmail.com - 2018-11-22 22:33 -0800
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-23 10:34 +0100
Re: Niezmienniki pętli Maciej Sobczak <see.my.homepage@gmail.com> - 2018-11-23 05:46 -0800
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-23 15:39 +0100
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-23 15:42 +0100
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-23 15:47 +0100
Re: Niezmienniki pętli Wojciech Muła <wojtek.mula@gmail.com> - 2018-11-23 10:54 -0800
Re: Niezmienniki pętli Borneq <borneq@antyspam.hidden.pl> - 2018-12-01 15:15 +0100
Re: Niezmienniki pętli Wojciech Muła <wojtek.mula@gmail.com> - 2018-12-01 11:50 -0800
Re: Niezmienniki pętli Borneq <borneq@antyspam.hidden.pl> - 2018-12-02 13:52 +0100
Re: Niezmienniki pętli Maciej Sobczak <see.my.homepage@gmail.com> - 2018-11-24 12:20 -0800
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-23 15:53 +0100
Re: Niezmienniki pętli Maciej Sobczak <see.my.homepage@gmail.com> - 2018-11-24 12:05 -0800
Re: Niezmienniki pętli Wojciech Muła <wojtek.mula@gmail.com> - 2018-11-26 02:01 -0800
Re: Niezmienniki pętli szykcech@gmail.com - 2018-11-23 08:42 -0800
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-23 19:42 +0100
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-23 19:43 +0100
Re: Niezmienniki pętli Wojciech Muła <wojtek.mula@gmail.com> - 2018-11-22 23:00 -0800
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-23 10:38 +0100
Re: Niezmienniki pętli Wojciech Muła <wojtek.mula@gmail.com> - 2018-11-23 04:08 -0800
Re: Niezmienniki pętli Wojciech Muła <wojtek.mula@gmail.com> - 2018-11-23 04:10 -0800
Re: Niezmienniki pętli AK <nobody@nowhere.net> - 2018-11-23 15:33 +0100
Re: Niezmienniki pętli Maciej Sobczak <see.my.homepage@gmail.com> - 2018-11-20 05:38 -0800
Re: Niezmienniki pętli godek.maciek@gmail.com - 2018-11-21 11:32 -0800
Re: Niezmienniki pętli Maciej Sobczak <see.my.homepage@gmail.com> - 2018-11-21 13:28 -0800
Re: Niezmienniki pętli godek.maciek@gmail.com - 2018-11-21 14:04 -0800
Re: Niezmienniki pętli Maciej Sobczak <see.my.homepage@gmail.com> - 2018-11-22 02:31 -0800
Re: Niezmienniki pętli fir <profesor.fir@gmail.com> - 2018-11-22 06:22 -0800
Re: Niezmienniki pętli Sebastian Biały <heby@poczta.onet.pl> - 2018-11-22 18:53 +0100
Re: Niezmienniki pętli queequeg@trust.no1 (Queequeg) - 2018-11-19 09:45 +0000
Re: Niezmienniki pętli Maciej Sobczak <see.my.homepage@gmail.com> - 2018-11-20 05:29 -0800
Re: Niezmienniki pętli queequeg@trust.no1 (Queequeg) - 2018-11-20 22:26 +0000
Re: Niezmienniki pętli Maciej Sobczak <see.my.homepage@gmail.com> - 2018-11-29 00:08 -0800
Page 5 of 5 — ← Prev page 1 2 3 4 [5]
| From | Maciej Sobczak <see.my.homepage@gmail.com> |
|---|---|
| Date | 2018-11-20 05:38 -0800 |
| Message-ID | <1ce1983c-fa20-4a50-9a81-f56b0ac340ef@googlegroups.com> |
| In reply to | #32023 |
> Warto przyjrzeć się językowi Idris i typom zależnym. Nie przekonują mnie. Jeśli je rozumiem, to typy zależne pozwalają związać warunki między parametrami i wartością zwracaną z funkcji. Fajnie, ale to nie wyczerpuje tematu, bo jest jeszcze stan (również globalny), który też mogę chcieć związać takimi warunkami. Co więcej, takie warunki nie muszą mieć związku z typami - np. jedna metoda w obiekcie może "obiecać" inne warunki końcowe, niż inna metoda, a przecież nie jest tak, że typ obiektu jest różny w różnych metodach. Takie ograniczenie już na poziomie terminologii wskazuje, że typy zależne to domena jakiejś niszy językowej (w szczególności języków funkcjonalnych), więc od razu ma dla mnie ograniczoną stosowalność. Potrzebny jest inny formalizm. Pre- i post-conditions wydają się być bardziej niekonfliktowym mechanizmem, tzn. możliwym do zastosowania bez niepotrzebnych ograniczeń. -- Maciej Sobczak * http://www.inspirel.com
[toc] | [prev] | [next] | [standalone]
| From | godek.maciek@gmail.com |
|---|---|
| Date | 2018-11-21 11:32 -0800 |
| Message-ID | <880e90bd-f135-4b7b-aebd-46892a961cfb@googlegroups.com> |
| In reply to | #32038 |
W dniu wtorek, 20 listopada 2018 14:38:53 UTC+1 użytkownik Maciej Sobczak napisał: > > Warto przyjrzeć się językowi Idris i typom zależnym. > > Nie przekonują mnie. Jeśli je rozumiem, to typy zależne pozwalają związać warunki między parametrami i wartością zwracaną z funkcji. Fajnie, ale to nie wyczerpuje tematu, bo jest jeszcze stan (również globalny), który też mogę chcieć związać takimi warunkami. Nie wiem, czy to wyczerpuje temat, ale na pewno jest przykładem czegoś, co zwiększa ilość rzeczy, które możemy statycznie powiedzieć o naszym programie. Tutaj jest prezentacja o tym, w jaki sposób typy zależne umożliwiają wyrażanie błędów w programach (na przykładzie Heartbleed, przy użyciu Liquid Haskell): https://www.youtube.com/watch?v=YByOdE-YUwY > Co więcej, takie warunki nie muszą mieć związku z typami - np. jedna metoda w obiekcie może "obiecać" inne warunki końcowe, niż inna metoda, a przecież nie jest tak, że typ obiektu jest różny w różnych metodach. Takie ograniczenie już na poziomie terminologii wskazuje, że typy zależne to domena jakiejś niszy językowej (w szczególności języków funkcjonalnych), więc od razu ma dla mnie ograniczoną stosowalność. Ja nie jestem co do tego przekonany. Tzn. mnie się to też nie wydaje naturalne, ale często "naturalność" to po prostu kwestia przyzwyczajenia. > Potrzebny jest inny formalizm. Pre- i post-conditions wydają się być bardziej niekonfliktowym mechanizmem, tzn. możliwym do zastosowania bez niepotrzebnych ograniczeń. Jest też język ATS (trochę protoplasta Rusta), który ma system "typów liniowych" służących do wyrażania twierdzeń o poprawności korzystania z zasobów. Ale wydaje się raczej trudny do używania: https://www.youtube.com/watch?v=zt0OQb1DBko
[toc] | [prev] | [next] | [standalone]
| From | Maciej Sobczak <see.my.homepage@gmail.com> |
|---|---|
| Date | 2018-11-21 13:28 -0800 |
| Message-ID | <1883ef68-7e92-469d-a51a-214c984a341b@googlegroups.com> |
| In reply to | #32052 |
> Nie wiem, czy to wyczerpuje temat, ale na pewno jest > przykładem czegoś, co zwiększa ilość rzeczy, które możemy > statycznie powiedzieć o naszym programie. Zwiększa względem czego? Względem w ogóle braku takich mechizmów? Tak. Jest to postęp. Względem pre- i post-conditions? Nie widzę tego. 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. > Jest też język ATS (trochę protoplasta Rusta), który > ma system "typów liniowych" służących do wyrażania twierdzeń > o poprawności korzystania z zasobów. Ale wydaje się raczej > trudny do używania: Skoro jest trudny, to tym bardziej nie ma szans na rynkową akceptację. -- Maciej Sobczak * http://www.inspirel.com
[toc] | [prev] | [next] | [standalone]
| From | godek.maciek@gmail.com |
|---|---|
| Date | 2018-11-21 14:04 -0800 |
| Message-ID | <ac668671-6ccf-476b-8552-246b5658a767@googlegroups.com> |
| In reply to | #32055 |
W dniu środa, 21 listopada 2018 22:28:05 UTC+1 użytkownik Maciej Sobczak napisał: > > Nie wiem, czy to wyczerpuje temat, ale na pewno jest > > przykładem czegoś, co zwiększa ilość rzeczy, które możemy > > statycznie powiedzieć o naszym programie. > > Zwiększa względem czego? > Względem w ogóle braku takich mechizmów? Tak. Jest to postęp. > Względem pre- i post-conditions? Nie widzę tego. Co masz na myśli mówiąc o pre- i post-conditions? Jaki język? > 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ć. > > Jest też język ATS (trochę protoplasta Rusta), który > > ma system "typów liniowych" służących do wyrażania twierdzeń > > o poprawności korzystania z zasobów. Ale wydaje się raczej > > trudny do używania: > > Skoro jest trudny, to tym bardziej nie ma szans na rynkową akceptację. Nie ma żadnych szans. To jest risercz, i wcale nie udaje, że próbuje być czymś więcej. Ale może można stamtąd wydobyć jakieś wartościowe pomysły.
[toc] | [prev] | [next] | [standalone]
| From | Maciej Sobczak <see.my.homepage@gmail.com> |
|---|---|
| Date | 2018-11-22 02:31 -0800 |
| Message-ID | <96c2de02-3f43-405f-a81f-235a050275e6@googlegroups.com> |
| In reply to | #32057 |
> 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
[toc] | [prev] | [next] | [standalone]
| From | fir <profesor.fir@gmail.com> |
|---|---|
| Date | 2018-11-22 06:22 -0800 |
| Message-ID | <5da8c76b-e9f9-461e-a4d8-764b314e031d@googlegroups.com> |
| In reply to | #32058 |
W dniu czwartek, 22 listopada 2018 11:31:21 UTC+1 użytkownik Maciej Sobczak napisał: > > 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 mz to duzo teorii nie rokujacej na spektakularne efekty... jesli zajmowac sie teoria to polecam jakas lepsza...np to co mowilem o obsludze bledow w poprawionym c z ta klauzula on_error duzo lepsze bo teoria trzeba sie zajmowac albo porzadna albo lepiej wcale i lepiej pisac jakis konkretny kod zaluje ze nie rozmawia sie tu o konkretnych problemach z kodu... np godek jesli by naswietlil jakie ma problemy z tymi figurkami w 3d i co konkretnie chce zrobic moze po zastanowieniu sie ozna by cos obgadac.. sam jak pisalem sam troche chcialbym sie zajmowac czyms podobnym (miedzy innymi() tyle ze u mie to nie tyle wzgledby ruch/mechanika czesci w jakiejs figurce 3d tylko raczej fajne dobrze wygladajace ruchy/mechanika tych obiektow w przestrzeni - bo dzis ruchy obiektow w 3d nawet w grach AAA wygladaja mi na predefiniowane i toporne...fajnie by bylo zrobic cos co naprawde by sie dobrze ruszalo ;c z tym ze w sumie nie wiem czy mam na to czas
[toc] | [prev] | [next] | [standalone]
| From | Sebastian Biały <heby@poczta.onet.pl> |
|---|---|
| Date | 2018-11-22 18:53 +0100 |
| Message-ID | <pt6qf0$qq3$4@node2.news.atman.pl> |
| In reply to | #32017 |
On 19/11/2018 08:14, Maciej Sobczak wrote: > assert(dowolnyfragmentkodu, wynik_bool); > I użyć tego tak: > assert( > int i; // albo inne definicje Coverage i lint to widzą. Asercje przy statycznej analizie bywają niespełnialne a przy dynamicznej generują fałszywe wyniki pokrycia. Dlatego to musi by ficzer języka. Wiec nie tylko poszerzamy składnię ale musielibyśmy upoewnić się że takie narzędzia jak gcov i podobne nie zobaczą tego kodu nawet w debugu. Tak więc to troche złożony problem. Nie liczę że się kiedykolwiek doczekam.
[toc] | [prev] | [next] | [standalone]
| From | queequeg@trust.no1 (Queequeg) |
|---|---|
| Date | 2018-11-19 09:45 +0000 |
| Message-ID | <903199f9-c424-4ff4-9f5e-0dbc4d23ebe7@trust.no1> |
| In reply to | #32013 |
Sebastian Biały <heby@poczta.onet.pl> wrote: > To następna obserwacja: jeśl wpływa to na runtime release należy to > odrzucić. Wszelakie checkery asercyjne, za wyjątkiem programowania > defensywanego, nie mogą istnieć w kodzie produkcyjnym. Nigdy nie rozumiałem sensu tego rozumowania (poza kodem, w którym prędkość wykonania jest tak krytyczna, że nawet asercje go opóźniają). Byłoby idealnie, gdyby na produkcję szedł kod bez błędów, ale nigdy tak nie jest... > Dlatego używam np metaprogramowania do kontrolownia różych obliczeń. > Jednak dalej brakuje mi czegoś takiego jak int a<4-200> i kontroli > komilatora w debug kiedy a zmieni się poza zakres. Jakimś obejściem problemu jest opakowanie `a` w klasę... -- https://www.youtube.com/watch?v=9lSzL1DqQn0
[toc] | [prev] | [next] | [standalone]
| From | Maciej Sobczak <see.my.homepage@gmail.com> |
|---|---|
| Date | 2018-11-20 05:29 -0800 |
| Message-ID | <72ef19f9-4aaa-4a6b-9ffc-abb462a80c6d@googlegroups.com> |
| In reply to | #32020 |
> > To następna obserwacja: jeśl wpływa to na runtime release należy to > > odrzucić. Wszelakie checkery asercyjne, za wyjątkiem programowania > > defensywanego, nie mogą istnieć w kodzie produkcyjnym. > > Nigdy nie rozumiałem sensu tego rozumowania Sens jest również taki, że (jak na ironię!) w systemach krytycznych nie da się spełnić kryterium 100% pokrycia kodu testami czegoś, co ma asserta. Tzn. jeśli w kodzie jest assert, który *z założenia* ma się nigdy nie wykonać, to jest to tzw. dead code i ma go nie być. Bo jeśli jest, to nie da się go przetestować. Albo inaczej: nie da się wykazać testami, że coś się nigdy nie wykona, więc nie da się zdobyć w ten sposób pewności, że się nie wykona. A jeśli osiągniemy tą pewność innymi metodami (np. formalnymi), to asserta dynamicznego może wtedy w ogóle nie być. Zupełnie niezależnie od tego, w pewnych środowiskach walnięcie assertem jest bez sensu, bo i tak nie ma do kogo przekazać sterowania. Assert w rozruszniku serca jest bez sensu, nie tylko technicznie, ale też filozoficznie. To nie jest tylko kwestia szybkości działania, to może być też kwestia sensowności istnienia samego asserta. -- Maciej Sobczak * http://www.inspirel.com
[toc] | [prev] | [next] | [standalone]
| From | queequeg@trust.no1 (Queequeg) |
|---|---|
| Date | 2018-11-20 22:26 +0000 |
| Message-ID | <ba37322a-915b-41f5-b5c6-3ec5bb89be8c@trust.no1> |
| In reply to | #32037 |
Maciej Sobczak <see.my.homepage@gmail.com> wrote: >> > To następna obserwacja: jeśl wpływa to na runtime release należy to >> > odrzucić. Wszelakie checkery asercyjne, za wyjątkiem programowania >> > defensywanego, nie mogą istnieć w kodzie produkcyjnym. >> >> Nigdy nie rozumiałem sensu tego rozumowania > > Sens jest również taki, że (jak na ironię!) w systemach krytycznych nie > da się spełnić kryterium 100% pokrycia kodu testami czegoś, co ma > asserta. Tzn. jeśli w kodzie jest assert, który *z założenia* ma się > nigdy nie wykonać, to jest to tzw. dead code i ma go nie być. Bo jeśli > jest, to nie da się go przetestować. Albo inaczej: nie da się wykazać > testami, że coś się nigdy nie wykona, więc nie da się zdobyć w ten > sposób pewności, że się nie wykona. A jeśli osiągniemy tą pewność innymi > metodami (np. formalnymi), to asserta dynamicznego może wtedy w ogóle > nie być. To prawda. Ja (na szczęście -- bo odpowiedzialność jest ogromna) nigdy nie pisałem systemów krytycznych, ani nigdy u SQA nie robiło u nas tego typu testów (choć oczywiście to, co mówisz, ma sens). > Zupełnie niezależnie od tego, w pewnych środowiskach walnięcie assertem > jest bez sensu, bo i tak nie ma do kogo przekazać sterowania. Assert w > rozruszniku serca jest bez sensu, nie tylko technicznie, ale też > filozoficznie. To znów bardzo specyficzne zastosowanie i podejrzewam, że programowanie rozrusznika serca rządzi się swoimi regułami (raz, że jest to typowy układ embedded bez możliwości wyrzucenia błędu -- bo jak, w pulsie pacjenta zakodować linię kodu? -- a dwa, że jest to system krytyczny, w którym nieprawidłowa praca programu może powodować chorobę lub śmierć). Podejrzewam że pisząc oprogramowanie na rozruszniki serca stosuje się jakąś formę MISRA lub odpowiednik i że są tam jakieś sprzętowe failsafe'y, które uniemożliwiają przejście programowi w stan, który będzie zagrażał życiu lub zdrowiu. Tak to sobie przynajmniej wyobrażam. Z drugiej strony spotkałem się z systemem ładowania baterii (Li-Po), w którym zamiast dedykowanego kontrolera wyłączanie ładowarki było robione software'owo. Wszystko działało... do momentu, aż w systemie pojawił się błąd i zasilanie baterii nie było wyłączane po zakończeniu (nie wiem też co by było, gdyby urządzenie się zawiesiło). > To nie jest tylko kwestia szybkości działania, to może być też kwestia > sensowności istnienia samego asserta. Tak... czasem nie ma możliwości zaraportowania błędu i jest pytanie typu "ok, pojawił się błąd, ale co teraz?". Tylko właśnie -- co wtedy? Jeśli mogę sobie na to pozwolić i na danej platformie ma to sens, to staram się to w jakiś sposób zaraportować. Jeśli sensu ani możliwości nie ma, to pozostaje przestawienie wyjść w niegroźny stan i kontrolowany restart... i jeśli błąd nadal występuje, to tak w nieskończoność. Tak czy inaczej, jeśli system umożliwia jakieś zaraportowanie błędu lub ma możliwość interakcji z użytkownikiem, to używam tego. Zdarzało się, że tego typu asserty wyskakiwały na produkcji (choć teoretycznie kod był przetestowany przez SQA i teoretycznie nie powinny wyskoczyć). Dużo bardziej wolę dostać raport o błędzie wraz z tym, co wypluł program i co pozwala mi zdiagnozować błąd, niż pozwolić programowi działać dalej w stanie, w którym nie powinien się znaleźć. Nawet jeśli nie ma możliwości zaraportowania, to dużo bardziej wolę, jak program się zatrzymuje, a błąd jest jawny, niż jak błąd jest ukrywany i po jakimś czasie coś działa, ale nie tak jak powinno. Oczywiście nie pisząc oprogramowania na rozruszniki itd. systemy mogę sobie na to pozwolić -- awaria programu nie ma w tym przypadku skutków zdrowotnych (choć może mieć finansowe wynikające z braku możliwości używania programu). -- https://www.youtube.com/watch?v=9lSzL1DqQn0
[toc] | [prev] | [next] | [standalone]
| From | Maciej Sobczak <see.my.homepage@gmail.com> |
|---|---|
| Date | 2018-11-29 00:08 -0800 |
| Message-ID | <d0837337-f838-4745-a5bf-6c19739565a9@googlegroups.com> |
| In reply to | #31990 |
> Zastanawiam się, czy to jest pojęcie wyłącznie akademickie. Jeżeli ktoś po tej dyskusji ma jeszcze resztki zainteresowania tematem, to zachęcam do lektury: http://www.inspirel.com/articles/Supporting_Loop_Invariants.html To jest opis implementacji niezmienników - a konkretnie tego, jak można niezmienniki statycznie weryfikować. -- Maciej Sobczak
[toc] | [prev] | [standalone]
Page 5 of 5 — ← Prev page 1 2 3 4 [5]
Back to top | Article view | pl.comp.programming
csiph-web