-
Data: 2019-09-12 09:21:41
Temat: Re: Jak to robią w NASA
Od: Maciej Sobczak <s...@g...com> szukaj wiadomości tego autora
[ pokaż wszystkie nagłówki ]> 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.
[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ń.
[2] Przykładem takiego warunku jest np. to, co było pokazane dla funkcji max, albo
to, że funkcja sortująca faktycznie sortuje albo to, że funkcja abs nigdy nie zwróci
wartości ujemnej, itd. 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ń. 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.
--
Maciej Sobczak * http://www.inspirel.com
Następne wpisy z tego wątku
- 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 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 <=
- 2024-05-17 Warszawa => Senior Software Engineer PHP (BillPro) Contractor <=
- 2024-05-17 Warszawa => International freight forwarder <=