Typový system versus unittesty

[SB]

Proto me se libi treba clojure.spec. I kdyz je clojure dynamicky jazyk tak spec mu pridava neco jako "velmi silny typovy system" (Neni to primo v jazyku takze jsou potreba nejake nastroje na instrumentaci, proto "neco jako"). A krasne to integruje s testcheckem takze tomu muzu rict aby se pri buildu nahodne vygenerovalo bambilion vstupu odpovidajicich SPECifikaci a projelo se to funkci a vyhodnotilo jestli vystup taky odpovida specifikaci(a do znacne miry i jestli je spravne vzhledem ke konkretnim vstupum). Takze nemusim napsat jedinny unit test a mam pokryto radove lepe nez s unit testy.

Nepopisujete nic jiného než obdobu typového systému či jednotkového testu - z popisu nejde pozdnat, čemu je to blíže. Představa, že za vás nějaký jednoduchý systém bezpracně otestuje funkcionalitu, je nesmyslná.

[Reklama]

[JSH]

S reálnými čísly by to šlo taky, pokud by program skutečně pracoval s reálnými hodnotami. S něčím takovým jsem se setkal pouze u analogového počítače, což už je docela historie.

Co přesně myslíš těma "reálnýma hodnotama"? I analogové počítače měly jenom omezenou přesnost, takže i tam může nastat ztráta přesnosti.

[Kit]

S reálnými čísly by to šlo taky, pokud by program skutečně pracoval s reálnými hodnotami. S něčím takovým jsem se setkal pouze u analogového počítače, což už je docela historie.

Co přesně myslíš těma "reálnýma hodnotama"? I analogové počítače měly jenom omezenou přesnost, takže i tam může nastat ztráta přesnosti.

Správně. V tom případě mohu s klidným svědomím prohlásit, že současné počítače s reálnými čísly nepracují. Pouze s čísly celými a racionálními. Racionální čísla jsou podílem celých čísel. Že se používají pojmy integer, decimal, float nebo complex znamená jen to, že jsme je potřebovali rozlišit v dřevních dobách, kdy se šetřilo každým bajtem. Dnešní programy však už umí pracovat s racionálními čísly téměř s neomezenou přesností. Otázkou však zůstává, k čemu by to bylo.

[SB]

V praxi to pak bude vypadat tak, že v záhlaví testované metody budou definovány tyto okrajové podmínky. Pak už nebude nutné testy generovat do dalších souborů, ale budou se přímo interpretovat z těchto záhlaví. Přiblíží se tak k typovým signaturám, ale budou dokonalejší. Pro některé jazyky to už více či méně funguje.

To jako toto? https://en.wikipedia.org/wiki/Design_by_contract To je jen chytřejší variantou jednoduchých typů. Jednotkové testy tím nejde nahradit, protože tím nejde udělat test "když je na vstupu něco, bude na výstupu něco".

[SB]

Jenže kompilátor neví nic o kvadratických rovnicích, takže to z typů nijak neodvodí. Ale to je právě ten spor, který tady vedeme – existují určité doménové znalosti, a část z nich je přenesena do kódu, ať už v podobě příkazů nebo pravidel. Jednotkové testy nejsou nic jiného, než snaha nezávislým způsobem ověřit, že jsou ty doménové znalosti přenesené do kódu správně. Vedlejším efektem těchto testů je, že se zkontroluje, zda vůbec dává smysl kód sám o sobě – jestli se třeba nepokouší provádět nedefinovanou operaci (třeba násobení textů nebo dělení nulou). Někteří zde ovšem tento vedlejší efekt testů považují za jejich hlavní a jediný účel, z čehož plyne jejich přesvědčení, že by se jednotkové testy vlastně daly úplně zrušit.

Mimochodem, k představě, že všechny jednotkové testy bude umět vytvořit nějaký automat, je vhodné dodat, že až ten automat bude umět pochopit danou doménu a napsat testy, bude umět naprogramovat i ten výkonný kód.

Tento komentář považuju za shrnující. Nenapadá mě, co dodat.

[Reklama]

[v]

Jenže kompilátor neví nic o kvadratických rovnicích, takže to z typů nijak neodvodí. Ale to je právě ten spor, který tady vedeme – existují určité doménové znalosti, a část z nich je přenesena do kódu, ať už v podobě příkazů nebo pravidel. Jednotkové testy nejsou nic jiného, než snaha nezávislým způsobem ověřit, že jsou ty doménové znalosti přenesené do kódu správně. Vedlejším efektem těchto testů je, že se zkontroluje, zda vůbec dává smysl kód sám o sobě – jestli se třeba nepokouší provádět nedefinovanou operaci (třeba násobení textů nebo dělení nulou). Někteří zde ovšem tento vedlejší efekt testů považují za jejich hlavní a jediný účel, z čehož plyne jejich přesvědčení, že by se jednotkové testy vlastně daly úplně zrušit.

Mimochodem, k představě, že všechny jednotkové testy bude umět vytvořit nějaký automat, je vhodné dodat, že až ten automat bude umět pochopit danou doménu a napsat testy, bude umět naprogramovat i ten výkonný kód.

Tento komentář považuju za shrnující. Nenapadá mě, co dodat.

naopak by šlo ubrat, stačila by jenom první věta

[Kit]

V praxi to pak bude vypadat tak, že v záhlaví testované metody budou definovány tyto okrajové podmínky. Pak už nebude nutné testy generovat do dalších souborů, ale budou se přímo interpretovat z těchto záhlaví. Přiblíží se tak k typovým signaturám, ale budou dokonalejší. Pro některé jazyky to už více či méně funguje.

To jako toto? https://en.wikipedia.org/wiki/Design_by_contract To je jen chytřejší variantou jednoduchých typů. Jednotkové testy tím nejde nahradit, protože tím nejde udělat test "když je na vstupu něco, bude na výstupu něco".

Ne, v daném případě mám na mysli tohle:

Kód: [Vybrat]

<?php
class Calculator {
    /**
     * @assert (0, 0) == 0
     * @assert (3, 5) == 8
     * @assert (-3, 5) == 2
     * @assert (3, -5) == -2
     * @assert (-3, -5) == 8
     */
    public function sum($a, $b) {
        return $a + $b;
    }
}
Z tohoto kódu se dnes běžně generují testy, ovšem stejně dobře se z toho dají přímo interpretovat.

[JSH]

Správně. V tom případě mohu s klidným svědomím prohlásit, že současné počítače s reálnými čísly nepracují. Pouze s čísly celými a racionálními. Racionální čísla jsou podílem celých čísel. Že se používají pojmy integer, decimal, float nebo complex znamená jen to, že jsme je potřebovali rozlišit v dřevních dobách, kdy se šetřilo každým bajtem. Dnešní programy však už umí pracovat s racionálními čísly téměř s neomezenou přesností. Otázkou však zůstává, k čemu by to bylo.

No ale o to mi jde. Jak pak ten typový systém může porovnávat nějaké výpočty? Jak může zkontrolovat že nějaký vzoreček tu kvadratickou rovnici opravdu řeší? Symbolickým dosazováním nějaké katastrofické krácení neodhalí.

[listoper]

Proto me se libi treba clojure.spec. I kdyz je clojure dynamicky jazyk tak spec mu pridava neco jako "velmi silny typovy system" (Neni to primo v jazyku takze jsou potreba nejake nastroje na instrumentaci, proto "neco jako"). A krasne to integruje s testcheckem takze tomu muzu rict aby se pri buildu nahodne vygenerovalo bambilion vstupu odpovidajicich SPECifikaci a projelo se to funkci a vyhodnotilo jestli vystup taky odpovida specifikaci(a do znacne miry i jestli je spravne vzhledem ke konkretnim vstupum). Takze nemusim napsat jedinny unit test a mam pokryto radove lepe nez s unit testy.

Nepopisujete nic jiného než obdobu typového systému či jednotkového testu - z popisu nejde pozdnat, čemu je to blíže. Představa, že za vás nějaký jednoduchý systém bezpracně otestuje funkcionalitu, je nesmyslná.

Nechapu. Prece tam sam pisu ze je to neco jako typovy system.  A nemam ani zminovanou predstavu.

[andy]

Jenže kompilátor neví nic o kvadratických rovnicích, takže to z typů nijak neodvodí

Ale kompilátor může vědět něco o symbolické matematice a nějaké další matematické axiomy ho můžeme naučit. Pokud bychom měli typový systém, který by uměl symolickou matematiku, tak jaký je problém napsat něco typu:

Kód: [Vybrat]

resKvadRovnici :: a : Num -> b : Num -> c : Num -> [x] | a * x^2 + b * x + c * x = 0
A systémy, které umí symbolickou matematiku tady máme a když se jich zeptáme, jestli daný vzoreček řeší kvadratickou rovnici, tak jsou schopny na to dát jasnou odpověď. Ne vždycky (halting problem), ale o to nejde.

Konec konců, ten příklad s leftPad je moc hezký - copak typový systém ví něco o zarovnávání z leva? Ale dá se mu to vysvětlit.

Ale myslím, že je trošku nepochopení, k čemu typový systém je. Byl tady dotaz, že jak testovat v tom mém příkladu, že u:

Kód: [Vybrat]

Num op a b = op a b
nedošlo k prohození "a" a b". Jenomže to jde otestovat leda tak, že se napíše specifikace, která bude vypadat přesně stejně. Takže se problém chyby přesune od kódu ke specifikaci a vůbec nic to nevyřeší, jen místo toho, zda kód je správně budeme řešit, jestli specifikace je správně. IMO typový systém (nebo obecně dokazování) má smysl tam, kde specifikace a kód není totéž. Ale jinak bych zopakoval, že u všech těchto věcí (testy, typy) je vhodné si položit otázku, zda se to vyplatí - a při dobrém využití typů (na doméně, kde to funguje dobře) výhoda těch testů dost klesá, protože těch chyb je tam z principu výrazně méně.

[SB]

Ne, v daném případě mám na mysli tohle:

Kód: [Vybrat]

<?php
class Calculator {
    /**
     * @assert (0, 0) == 0
     * @assert (3, 5) == 8
     * @assert (-3, 5) == 2
     * @assert (3, -5) == -2
     * @assert (-3, -5) == 8
     */
    public function sum($a, $b) {
        return $a + $b;
    }
}
Z tohoto kódu se dnes běžně generují testy, ovšem stejně dobře se z toho dají přímo interpretovat.

Supr, tak se začínáme blížit k těm jednotkovým testům, ale ještě tam nejsme, protože tato notace neřeší stav objektu, na kterém je výsledek té metody/funkce závislý (myšleno obecně, ne této triviální funkcičky). Generátor Rand tím taky neotestujete.

[SB]

Proto me se libi treba clojure.spec. I kdyz je clojure dynamicky jazyk tak spec mu pridava neco jako "velmi silny typovy system" (Neni to primo v jazyku takze jsou potreba nejake nastroje na instrumentaci, proto "neco jako"). A krasne to integruje s testcheckem takze tomu muzu rict aby se pri buildu nahodne vygenerovalo bambilion vstupu odpovidajicich SPECifikaci a projelo se to funkci a vyhodnotilo jestli vystup taky odpovida specifikaci(a do znacne miry i jestli je spravne vzhledem ke konkretnim vstupum). Takze nemusim napsat jedinny unit test a mam pokryto radove lepe nez s unit testy.

Nepopisujete nic jiného než obdobu typového systému či jednotkového testu - z popisu nejde pozdnat, čemu je to blíže. Představa, že za vás nějaký jednoduchý systém bezpracně otestuje funkcionalitu, je nesmyslná.

Nechapu. Prece tam sam pisu ze je to neco jako typovy system.  A nemam ani zminovanou predstavu.

Ale ten my už máme, teď potřebujeme nějaký lepší (ale snesitelně složitý!), ze kterého si sedneme na pr-del a zavrhneme jednotkové testy jako překonané (na to se přece v této diskusi čeká).

Hromadná kontrola se dá udělat několika způsoby:
- ručně tam ty páry vstup-výstup naboucháte - to nechcete
- použijete data driven testing, to je ale to samé, protože to taky odněkud ta data potřebuje získat - taky k hovnu
- znovuimplementujete výpočet stejně - bude to tentokrát bezchybné?
- znovuimplementujete výpočet jinak - to samé jako výše
Takže s tou o řád vyšší kvalitou protestování bych byl opatrný.

[Kit]

Supr, tak se začínáme blížit k těm jednotkovým testům, ale ještě tam nejsme, protože tato notace neřeší stav objektu, na kterém je výsledek té metody/funkce závislý (myšleno obecně, ne této triviální funkcičky). Generátor Rand tím taky neotestujete.

Tohle je jen primitivní ukázka, jak se dají jednotkové testy vložit do jazyka, který s nimi původně vůbec nepočítal. Tahle testuje bezstavovou metodu. Není to test jednotkový, ale vývojářský. Podobný test, tentokrát jednotkový a stavový, se dá vložit do záhlaví třídy. Nevýhodou tohoto řešení však je, že testy bývají zhruba 2× delší než produkční kód, po kompilaci na produkci v něm stále překáží - jsou součástí binárky.

V Javě je to o něco lepší - tam se dá test vložit přes statickou vnitřní třídu, která však do produkce nejde. Ovšem už se to nepodobá zmíněným typům.

[Filip Jirsák]

Ale kompilátor může vědět něco o symbolické matematice a nějaké další matematické axiomy ho můžeme naučit.

Ano, některé věci můžeme schovat do knihoven a knihovny klidně do kompilátoru nebo až do procesoru. Ty pak bereme za dané a podle míry jejich složitosti už je ani netestujeme. Programátoři dnes obvykle neprogramují, jak sečíst dvě 32bitová čísla, ale spoléhají na to, že to instrukce procesoru děla správně. Pořád je ale potřeba programátor na to, aby procesoru „vysvětlil“, že když má v jednom registru částku a v druhém registru DPH, cenu s DPH spočítá právě sečtením těch dvou registrů.

A systémy, které umí symbolickou matematiku tady máme a když se jich zeptáme, jestli daný vzoreček řeší kvadratickou rovnici, tak jsou schopny na to dát jasnou odpověď. Ne vždycky (halting problem), ale o to nejde.

Ano, ale k tomu musíme umět tou symbolickou matematikou popsat, co je to kvadratická rovnice. A pokud tomu systému popíšu kvadratickou rovnici jako součet násobku druhé mocniny proměnné a násobku proměnné, tj. zapomenu na to, že v kvadratické rovnici může být také konstanta, ten systém to nijak nezjistí. V systému symbolické matematiky je taková rovnice možná, je to podmnožina kvadratických rovnic. A není to chyba toho systému ani odvozování, je to chyba v převodu mezi reálným světem a formálním jazykem (v tomto případě symbolickou matematikou).

Konec konců, ten příklad s leftPad je moc hezký - copak typový systém ví něco o zarovnávání z leva? Ale dá se mu to vysvětlit.

Ano, naprogramovat se dá leccos, i mnohem složitější věci, než je zarovnávání zleva :-) A jsou různé způsoby, jak to naprogramovat, dá se to naprogramovat imperativně i deklarativně a je to vzájemně převoditelné. Rozdíl není na straně počítače (i když fakticky se nakonec vše převádí na imperativní, protože tak pracují dnešní procesory), rozdíl je na straně lidí – některé věci se nám lépe vyjadřují deklarativně, některé raději vyjadřujeme imperativně.

Ale myslím, že je trošku nepochopení, k čemu typový systém je.

Taky si myslím. Typový systém je jen jiný způsob vyjádření, nic míň, ale ani nic víc.

Jenomže to jde otestovat leda tak, že se napíše specifikace, která bude vypadat přesně stejně. Takže se problém chyby přesune od kódu ke specifikaci a vůbec nic to nevyřeší, jen místo toho, zda kód je správně budeme řešit, jestli specifikace je správně.

Ano, to tvrdím od začátku. Takhle se to ale dá odsouvat do nekonečna, a o správnosti se nedozvíme nikdy nic. Proto se často testuje to, že vezmu něco mnohem jednoduššího, než specifikaci, o čem ale vím, že je to správně, a otestuju jenom tyhle zaručeně správné případy. Tím nezískám odpověď na otázku, zda je to celé správně, ale dozvím se alespoň to, že tam je aspoň něco správně.

IMO typový systém (nebo obecně dokazování) má smysl tam, kde specifikace a kód není totéž. Ale jinak bych zopakoval, že u všech těchto věcí (testy, typy) je vhodné si položit otázku, zda se to vyplatí - a při dobrém využití typů (na doméně, kde to funguje dobře) výhoda těch testů dost klesá, protože těch chyb je tam z principu výrazně méně.

A stejně tak existují domény, kde nesou potřeba žádné složité typy a kde zároveň největší množství chyb vzniká při převodu mezi neformálním zadáním a formálním programovacím jazykem. A tam je zase minimum chyb, které by bylo možné odstranit lepšími typy.

[Phi]

Halting problem se týká univerzálního algoritmu který by dokázal pro jakýkoliv program s jakýmkoliv vstupem rozhodnout, zda dokončí nebo nedokončí běh. Turing nikdy neřekl, že neexistuje algoritmus, který by pro konkrétní program nedokázal rozhodnout, zda dokončí či nedokončí. To je velký rozdíl.

Zjevně jsi nepřečetl ten odstavec, který jsem doporučoval:

The halting problem is theoretically decidable for linear bounded automata (LBAs) or deterministic machines with finite memory. Minsky warns us, however, that machines such as computers with e.g., a million small parts, each with two states, will have at least 21,000,000 possible states: This is a 1 followed by about three hundred thousand zeroes ... Even if such a machine were to operate at the frequencies of cosmic rays, the aeons of galactic evolution would be as nothing compared to the time of a journey through such a cycle.

V dněšních počítačích a běžných programech je těch stavů ještě o mnoho řádů více. Mnoho štěstí s testováním.

A drtivá většina z těch stavů je irrelevantních nebo je lze považovat za víceméně duplicity.
Při testování mne typicky nezajímá, jestli je program otestován při kompilaci na na adresu 0, na adresu 1, na adresu 2 nebo na adresu 10000000. Stejně tak mne nezajímá, jestli je o testován na jádru 1, na jádru 2, nebo kam nahrál OS runtime knihovny. Zajímají mne stavy možné v doméně jazyka v kterém programuji.
Jiný příklad je ten random(), ten se taky netestuje výčtem stavů, ale tím že na vzorku pustím statistické testy. Překvapivě to funguje, i když podle vás by nemělo.