W dniu piątek, 16 listopada 2018 09:27:41 UTC+1 użytkownik Maciej Sobczak napisał:
> Zastanawiam się, czy to jest pojęcie wyłącznie akademickie.
>
> W tzw. "normalnym" programowaniu, które praktykuje większość programistów, nigdy
nie widziałem odwołania się do takiej koncepcji w sensie wykorzystania niezmienników
w projektowaniu kodu.
> Jak programista ma do napisania pętlę, to w praktyce:
> - albo już pisał podobną i napisze jeszcze raz (to jest najczęstszy przypadek),
> - albo nie pisał, ale rozumie i napisze posługując się głównie intuicją (wtedy mamy
frajdę, bo coś nowego),
> - albo nie rozumie i nie napisze.
>
> Niezmienniki pozwalają jednak pętlę zaprojektować albo przeanalizować i np. dojść
do wniosku, że jest poprawna.
> Nie pytam o metody formalne, tylko o powiedzmy nieco bardziej świadomą praktykę
programistyczną. Nazwijmy to ładnie "attentive engineering". Albo "mindful
engineering".
>
> Pytanie jest takie: czy ktoś z Was spotkał się z tym pojęciem (poza szkołą) a nawet
z niego skorzystał w praktyce? Czy to jest praktyka, do której staracie się sięgać w
tym trzecim przypadku? A może bardziej regularnie?
>
> Czy może po prostu w ogóle temat jest oderwany od tzw. rzeczywistości?
>
> Ciekawi mnie Wasze spojrzenie na tą sprawę również wtedy, gdy piszecie w językach
nie-imperatywnych, gdzie takich klasycznych pętli jest mniej albo w ogóle ich nie ma.
Czy w związku z tym zagadnienie niezmienników jest niepotrzebne? A może nadal jest
potrzebne i coś innego je zastępuje?
>
> Wersja dla quizowiczów:
> - wiem i używam albo pamiętam, że mogę,
> - słyszałem i ignoruję,
> - nie rozumiem pytania[*].
>
> [*] https://en.wikipedia.org/wiki/Loop_invariant
>
> --
> Maciej Sobczak * http://www.inspirel.com

Kevlin Henney poruszył ten temat w jednej z prezentacji,
pokazując związek logiki Hoare'a z "metodyką" "given-when-then"
stosowaną przy pisaniu testów:

https://www.youtube.com/watch?v=JiQct3QixMo

Jeżeli idzie o mnie, to zastanawianie się nad "warunkami początkowymi"
i "warunkami końcowymi" wydaje mi się dziwne. I o ile wyrażanie własności
programów wydaje mi się ważnym skillem (np. w połączeniu z model-checkerami
albo property-based testing), i dostrzegam pewną wartość w akademickich
narzędziach pokroju ATS i liniowych systemach typów, o tyle pytanie
o niezmienniki pętli jest dla mnie po prostu nienaturalną formą
rozumowania.

(Ale też jeśli mam wybór, wolę myśleć w oparciu o równania rekurencyjne,
niż imperatywne pętle)