Re: Jak to robią w NASA

Newsgroups	pl.comp.programming
Date	2019-09-12 03:05 -0700
References	(18 earlier) <efda217d-c77f-474c-9528-f27c49f9bf99@googlegroups.com> <99f5c150-31a7-4000-8c3d-a484031d5d09@googlegroups.com> <c8902034-b5ff-4228-a999-6c48b98e64e6@googlegroups.com> <6a2729e1-09f4-4c24-be01-1c6fede2c4f3@googlegroups.com> <bdc3f3c2-7fd5-4cf2-b842-22bb04a48272@googlegroups.com>
Message-ID	<22902c8a-9482-453a-970c-c1cd5dbacf47@googlegroups.com> (permalink)
Subject	Re: Jak to robią w NASA
From	"M.M." <mmarszik@gmail.com>

Show all headers | View raw

On Thursday, September 12, 2019 at 9:21:42 AM UTC+2, Maciej Sobczak wrote:
> > A konkretnie, co jest na temat a co nie jest i na jaki?
> 
> Pół dyskusji w tym wątku było nie na temat tego wątku.
> 
> > Nie wiem co to
> > jest "verification condition".
> 
> To jest coś, co zakładamy[1], że jest prawdą albo co musi być wykazane[2], 
> że jest prawdą, żeby program uznać za poprawny.

Na razie rozumiem, że "verification condition" to jest cokolwiek z czego
prawdziwości wynika poprawność programu, albo czego prawdziwości jest 
tożsama z poprawnością programu. Coś w rodzaju 
X => Y
X <=> Y
Gdzie X to jest poprawny verification condition, a Y oznacza poprawność 
programu. 

Zwykle stosuję słabsze wnioskowanie, np. że z NIE prawdziwości warunków 
testowych wynika że program jest nie poprawny. 

> [1] Przykładem takiego założenia jest np. zakres wartości typu int. Tego się 
> nie udowadnia, to się przyjmuje i dane z tego założenia są WEjściem dla 
> innych rozważań.

Tak, to chyba wynika z prawdziwości zdania "kompilator nie ma błędów".

> [2] Przykładem takiego warunku jest np. to, co było pokazane dla funkcji max, 

Tak, tamto zrozumiałem, choć do składni w adnotacjach bym musiał przywyknąć.

> albo to, że funkcja sortująca faktycznie sortuje albo to, że 
> funkcja abs nigdy nie zwróci wartości ujemnej, itd. 

Abs i sortowanie stanowią stosunkowo łatwe przykłady. Zwykle nie wiem 
jak mam zrobić warunki, gdy mam okienko dialogowe np. z 20ma polami i
piszę parser czy użytkownik nie wpisał blędnych wartości? Czy parser 
przepuści jakiś przypadek błędnych danych wejściowych dla programu? 
Niby sam parser jest takim warunkiem, działa na zasadzie: dane złe, to
warunek je wychwyci.

> Takich rzeczy nie wiemy z góry, ale możemy je wykazać (albo im 
> zaprzeczyć) wnioskując na podstawie informacji, które już znamy.
> 
> Fachowo, dowiedzenie, że VC (verification condition) jest spełnione nazywa się "discharge". Ale po polsku najlepiej powiedzieć, że jest "spełnione", bo "rozładowywanie warunków" brzmi głupio. Dowody mogą być automatyczne albo ręczne.
> 
> I teraz ciekawostka: asercja napisana przy użyciu makra "assert" może być
> traktowana jako warunek do wykazania *oraz* jako nowe założenie dla 
> dalszych rozważań. 

O jakie założenie i o jakie rozważania chodzi?

> W niektórych językach do tego drugiego celu służy konstrukcja "assume" i stosuje się ją wtedy, kiedy wiedza na jakiś temat pochodzi z zewnątrz - np. z tego, jak i gdzie dany program jest użytkowany.

Nie używałem assume. Widzę że w C/C++ microsofcie coś dodali:
https://docs.microsoft.com/en-us/cpp/intrinsics/assume?view=vs-2019

A w GCC zalecają sztuczki:
https://stackoverflow.com/questions/25667901/assume-clause-in-gcc
https://stackoverflow.com/questions/6031819/emulating-gccs-builtin-unreachable

Nie rozumiem, jakie są korzyści z dodania pustej funkcji, albo z operacji
bitowej AND z samymi jedynkami:
x = x & (~0);

Chociaż bezpieczniej byłoby OR z zerami:
x = x | 0;

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

Thread

Jak to robią w NASA Roman Tyczka <noemail@because.no> - 2019-08-30 09:09 +0200
  Re: Jak to robią w NASA Mateusz Viste <mateusz@wont.tell> - 2019-08-30 07:20 +0000
    Re: Jak to robią w NASA Roman Tyczka <noemail@because.no> - 2019-08-30 12:27 +0200
      Re: Jak to robią w NASA Mateusz Viste <mateusz@wont.tell> - 2019-08-30 11:09 +0000
        Re: Jak to robią w NASA slawek <x.y@org.org> - 2019-08-31 18:42 +0200
          Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-01 10:01 +0200
        Re: Jak to robią w NASA slawek <x.y@org.org> - 2019-08-31 18:52 +0200
      Re: Jak to robią w NASA slawek <x.y@org.org> - 2019-08-31 19:43 +0200
    Re: Jak to robią w NASA bartekltg <bartekltg@gmail.com> - 2019-09-04 07:39 -0700
  Re: Jak to robią w NASA queequeg@trust.no1 (Queequeg) - 2019-08-30 08:06 +0000
    Re: Jak to robią w NASA Mateusz Viste <mateusz@wont.tell> - 2019-08-30 12:49 +0000
      Re: Jak to robią w NASA slawek <x.y@org.org> - 2019-08-31 19:17 +0200
      Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-08-31 13:14 -0700
        Re: Jak to robią w NASA slawek <x.y@org.org> - 2019-08-31 22:44 +0200
          Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-08-31 13:54 -0700
          Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-08-31 14:15 -0700
        Re: Jak to robią w NASA queequeg@trust.no1 (Queequeg) - 2019-09-01 17:21 +0000
      Re: Jak to robią w NASA queequeg@trust.no1 (Queequeg) - 2019-09-01 17:17 +0000
    Re: Jak to robią w NASA Adam Klobukowski <adamklobukowski@gmail.com> - 2019-08-30 10:20 -0700
      Re: Jak to robią w NASA queequeg@trust.no1 (Queequeg) - 2019-09-01 17:23 +0000
  Re: Jak to robią w NASA Wojciech Muła <wojtek.mula@gmail.com> - 2019-08-30 10:21 -0700
    Re: Jak to robią w NASA slawek <x.y@org.org> - 2019-08-31 19:21 +0200
    Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-01 10:05 +0200
      Re: Jak to robią w NASA slawek <x.y@org.org> - 2019-09-04 17:38 +0200
        Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-04 19:10 +0200
  Re:Jak to robią w NASA slawek <x.y@org.org> - 2019-08-31 20:03 +0200
    Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-01 13:55 -0700
      Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-02 08:30 +0200
        Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-02 05:16 -0700
          Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-02 21:33 +0200
            Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-09-03 00:42 -0700
              Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-03 18:34 +0200
            Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-03 01:58 -0700
              Re: Jak to robią w NASA Roman Tyczka <noemail@because.no> - 2019-09-03 16:28 +0200
                Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-03 11:49 -0700
                Re: Jak to robią w NASA godek.maciek@gmail.com - 2019-09-03 12:33 -0700
                Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-04 00:31 -0700
                Re: Jak to robią w NASA godek.maciek@gmail.com - 2019-09-04 00:53 -0700
                Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-04 19:04 +0200
                Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-04 19:07 +0200
                Re: Jak to robią w NASA godek.maciek@gmail.com - 2019-09-04 10:54 -0700
                Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-04 21:07 +0200
                Re: Jak to robią w NASA godek.maciek@gmail.com - 2019-09-04 14:05 -0700
                Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-09-05 04:37 -0700
                Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-06 07:31 +0200
                Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-09-06 01:12 -0700
                Re: Jak to robią w NASA Mateusz Viste <mateusz@wont.tell> - 2019-09-06 08:33 +0000
                Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-09-06 03:06 -0700
                Re: Jak to robią w NASA Mateusz Viste <mateusz@wont.tell> - 2019-09-06 10:57 +0000
                Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-06 06:42 -0700
                Re: Jak to robią w NASA Mateusz Viste <mateusz@wont.tell> - 2019-09-06 14:06 +0000
                Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-06 12:03 -0700
                Re: Jak to robią w NASA Mateusz Viste <mateusz@wont.tell> - 2019-09-06 19:12 +0000
                Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-09-07 01:55 -0700
                Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-07 08:04 -0700
                Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-09-07 10:35 -0700
                Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-06 17:06 +0200
                Re: Jak to robią w NASA godek.maciek@gmail.com - 2019-09-06 16:48 -0700
                Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-08 08:13 +0200
                Re: Jak to robią w NASA godek.maciek@gmail.com - 2019-09-07 23:58 -0700
                Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-08 11:19 +0200
                Re: Jak to robią w NASA godek.maciek@gmail.com - 2019-09-08 03:13 -0700
                Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-09 17:56 +0200
                Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-09-08 02:36 -0700
                Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-06 17:11 +0200
                Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-09-06 09:22 -0700
                Re: Jak to robią w NASA godek.maciek@gmail.com - 2019-09-06 10:14 -0700
                Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-09-06 11:28 -0700
                Re: Jak to robią w NASA godek.maciek@gmail.com - 2019-09-06 14:59 -0700
                Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-04 14:49 -0700
                Re: Jak to robią w NASA godek.maciek@gmail.com - 2019-09-06 09:29 -0700
                Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-06 12:25 -0700
                Re: Jak to robią w NASA godek.maciek@gmail.com - 2019-09-06 14:00 -0700
                Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-07 08:21 -0700
                Re: Jak to robią w NASA godek.maciek@gmail.com - 2019-09-07 15:18 -0700
                Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-08 08:32 -0700
                Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-08 13:17 -0700
                Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-09-10 22:30 -0700
                Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-11 00:21 -0700
                Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-09-11 11:32 -0700
                Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-12 00:21 -0700
                Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-09-12 03:05 -0700
                Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-12 23:14 -0700
                Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-11 20:09 +0200
                Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-04 19:00 +0200
              Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-03 18:35 +0200
                Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-03 11:51 -0700
                Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-04 18:43 +0200
              Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-03 18:43 +0200
                Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-09-03 11:04 -0700
                Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-03 20:26 +0200
                Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-09-03 23:32 -0700
                Re: Jak to robią w NASA AK <nobody@nowhere.net> - 2019-09-04 18:52 +0200
                Re: Jak to robią w NASA "M.M." <mmarszik@gmail.com> - 2019-09-05 00:20 -0700
                Re: Jak to robią w NASA Maciej Sobczak <see.my.homepage@gmail.com> - 2019-09-03 12:05 -0700
              Re: Jak to robią w NASA slawek <x.y@org.org> - 2019-09-04 18:11 +0200
      Re: Jak to robią w NASA slawek <x.y@org.org> - 2019-09-04 18:00 +0200

csiph-web