Typový system versus unittesty

[Kit]

Kvadratická rovnice je definovaná jako ax^2 + bx +c = 0. Takže když se člověk zeptá "kompilátore, řeší tenhle vzoreček ax^2+bx+c=0, tak se ptá, jestli řeší kvadratickou rovnici jazykem, kterému kompilátor rozumí. Když tam dá jiný (neekvivalentní) vzoreček, tak se na to neptá.

Pořád jde jen o to, že kompilátor dokáže vyřešit jenom to, co má formálně a bezrosporně zadané. Jenže takováhle zadání programátoři obvykle nemají, ostatně je to jejich práce převádět neformální a neúplné zadání popsané přirozeným jazykem do formální a přesné řeči počítačů. V tomhle převodu se dělají chyby a je snaha těm chybám předcházet, mimo jiné i testováním.

No, takže fakt říkáte, že když kompilátor nepožádám, aby ověřil, že funkce řeší kvadratickou rovnici, tak to kompilátor neověří. Bingo.

Spíš se ptáme, jak ten kompilátor požádám, aby ověřil, že funkce řeší kvadratickou rovnici. Typem nebo testem? Jak bude vypadat zápis?

[Reklama]

[SB]

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.

Ale k čemu je to dobré, když jednotkové testy můžete vytvořit v jakémkoliv jazyku bez potřeby doplnění syntaxe či preprocesoru, a to při větší vyjadřovací schopnosti, protože není třeba vytvářet nový (aťto deklarativní či imperativní) jazyk, ale stačí ten vlastní.
Ono asi to (nepovinné) vyčlenění testů do extra kódu bude mít něco do sebe...

[andy]

Kvadratická rovnice je definovaná jako ax^2 + bx +c = 0. Takže když se člověk zeptá "kompilátore, řeší tenhle vzoreček ax^2+bx+c=0, tak se ptá, jestli řeší kvadratickou rovnici jazykem, kterému kompilátor rozumí. Když tam dá jiný (neekvivalentní) vzoreček, tak se na to neptá.

Pořád jde jen o to, že kompilátor dokáže vyřešit jenom to, co má formálně a bezrosporně zadané. Jenže takováhle zadání programátoři obvykle nemají, ostatně je to jejich práce převádět neformální a neúplné zadání popsané přirozeným jazykem do formální a přesné řeči počítačů. V tomhle převodu se dělají chyby a je snaha těm chybám předcházet, mimo jiné i testováním.

No, takže fakt říkáte, že když kompilátor nepožádám, aby ověřil, že funkce řeší kvadratickou rovnici, tak to kompilátor neověří. Bingo.

Spíš se ptáme, jak ten kompilátor požádám, aby ověřil, že funkce řeší kvadratickou rovnici. Typem nebo testem? Jak bude vypadat zápis?

No uměl bych si představit něco takového (hypoteticky):

Kód: [Vybrat]

getRoots :: a : Num -> b : Num -> c : Num -> [x] : [Num] | a * (x * x) + b * x + c = 0

Tohle je reálný příklad nějaké "vlastnosti" v liquid haskellu:

Kód: [Vybrat]

{-@ type NonEmpty a = {v:[a] | 0 < len v} @-}
{-@ group :: (Eq a) => [a] -> [ NonEmpty a ] @-}
group [] = []
group (x:xs) = (x:ys) : group zs
  where
    (ys,zs) = span (x ==) xs


[Filip Jirsák]

Kvadratická rovnice je definovaná jako ax^2 + bx +c = 0. Takže když se člověk zeptá "kompilátore, řeší tenhle vzoreček ax^2+bx+c=0, tak se ptá, jestli řeší kvadratickou rovnici jazykem, kterému kompilátor rozumí. Když tam dá jiný (neekvivalentní) vzoreček, tak se na to neptá.

No, a když si programátor bude myslet, že kvadratická rovnice je definovaná jako ax^2 + bx = 0, tak se zeptá „kompilátore, řeší tenhle vzoreček ax^2+bx=0?“, tak si bude myslet, že se ptá, jestli řeší kvadratickou rovnici, jazykem, kterému kompilátor rozumí. Programátor pak odevzdá naprogramovanou funkci pro výpočet kvadratické rovnice, kompilátor nebude hlásit žádnou chybu – akorát ta funkce bude ve spoustě případů počítat špatně.

No, takže fakt říkáte, že když kompilátor nepožádám, aby ověřil, že funkce řeší kvadratickou rovnici, tak to kompilátor neověří. Bingo.

Ne, kompilátor nepožádáte, aby ověřil, že funkce řeší kvadratickou rovnici. Protože kompilátor neví, co je kvadratická rovnice. Kompilátor ví, co je ax^2 + bx = 0 nebo ax^2 + bx + c = 0. Že něco z toho je kvadratická rovnice mu musí říct programátor. A může mu to říct špatně.

[listoper]

Kvadratická rovnice je definovaná jako ax^2 + bx +c = 0. Takže když se člověk zeptá "kompilátore, řeší tenhle vzoreček ax^2+bx+c=0, tak se ptá, jestli řeší kvadratickou rovnici jazykem, kterému kompilátor rozumí. Když tam dá jiný (neekvivalentní) vzoreček, tak se na to neptá.

No, a když si programátor bude myslet, že kvadratická rovnice je definovaná jako ax^2 + bx = 0, tak se zeptá „kompilátore, řeší tenhle vzoreček ax^2+bx=0?“, tak si bude myslet, že se ptá, jestli řeší kvadratickou rovnici, jazykem, kterému kompilátor rozumí. Programátor pak odevzdá naprogramovanou funkci pro výpočet kvadratické rovnice, kompilátor nebude hlásit žádnou chybu – akorát ta funkce bude ve spoustě případů počítat špatně.

Zatimco testem se to da vyresit lip, protoze ten co pise test prece vi, ze vysledek kvadraticke rovnice je (7, 10) nebo (12.333, -1).

[Reklama]

[JSH]

No uměl bych si představit něco takového (hypoteticky):

Kód: [Vybrat]

getRoots :: a : Num -> b : Num -> c : Num -> [x] : [Num] | a * (x * x) + b * x + c = 0


Tak pro inty by to fungovat hypoteticky mohlo. Ale pro floaty si nedokážu představit ani to, jak bych takovýhle předpis ověřoval sám. Minimálně bych tam musel přidat hromadu dalších předpokladů o vstupech a o požadované toleranci.

[JSH]

Zatimco testem se to da vyresit lip, protoze ten co pise test prece vi, ze vysledek kvadraticke rovnice je (7, 10) nebo (12.333, -1).

V testu se hlavně porovnávají dva diametrálně odlišné popisy. Tam je přece jenom menší šance, že by programátor udělal 2x podobnou chybu.

[SB]

Tato diskuse už tu nějaký ten den jede. Čím déle nad tím přemýšlím...

Pozor, další myšlenka!:

Použiju-li pro kontrolu jednoduchý typový systém, bude implementačně snadný, ale zároveň vlivem jeho širokých kategorií bude schopen POUZE v rámci těchto kategorií (tj. s jejich přesností) určit správnost výpočtu, což může dostačovat pouze na to, abych zjistil, zda jsem někde neudělal KONCEPČNÍ chybu.

Dokonalý typový systém (bez rozdílu na jeho druh), tj. takový, který přesně rozpozná chybu, by tedy musel mít kategorie mnohem užší (třeba až do kategorie pro každou hodnotu; včetně jejich vztahů), tedy by NĚJAKÝM způsobem musel duplikovat/nahrazovat testovaný výpočet, jinak by nebyl schopen posoudit správnost. Zduplikuju-li onen výpočet (bez ohledu na to, zda bude onen typový systém zapsaný deklarativně či imperativně), pak

1. to má smysl pouze tehdy, bude-li se to lišit, takže půjde o test porovnáním různých implementací,
2. musím počítat s obdobnou složitostí jako u původního výpočtu,
3. vlivem oné složitosti bude pravděpodobněji v tomto typovém systému chyba,
4. každopádně dělám 2x to samé (i když jinak)

ALE!

Jednotkový test sice jde napsat jako znovuimplementace výpočtu, ale nikdy takhle nebyl zamýšlen, protože by trpěl stejnými nevýhodami jako dokonalý typový systém. Proto na to jde opačně - nesnaží se o úplnost, tj. pokrytí všech vstupních kombinací, ale jen těch, u kterých s vysokou pravděpodobností očekává chybu, nebo které reprezentují typické hodnoty, a to tím nejpřímočařejším způsobem, tj. ověření konkrétního výstupu pro konkrétní vstup, čímž dosahuje vysoké efektivity vzhledem k složitosti potřebného aparátu.

Hadžime!

[BoneFlute]

Spíš se ptáme, jak ten kompilátor požádám, aby ověřil, že funkce řeší kvadratickou rovnici. Typem nebo testem? Jak bude vypadat zápis?

Ne, neptáme. Ptáme se kompilátoru typem. Tak zní zadání.

Ono asi to (nepovinné) vyčlenění testů do extra kódu bude mít něco do sebe...

A otázka zní, jaké to tedy má výhody? A dá se to napsat jinak? Typem?

Jednotkový test sice jde napsat jako znovuimplementace výpočtu, ale nikdy takhle nebyl zamýšlen, protože by trpěl stejnými nevýhodami jako dokonalý typový systém. Proto na to jde opačně - nesnaží se o úplnost, tj. pokrytí všech vstupních kombinací, ale jen těch, u kterých s vysokou pravděpodobností očekává chybu, nebo které reprezentují typické hodnoty, a to tím nejpřímočařejším způsobem, tj. ověření konkrétního výstupu pro konkrétní vstup, čímž dosahuje vysoké efektivity vzhledem k složitosti potřebného aparátu.

V testu se hlavně porovnávají dva diametrálně odlišné popisy. Tam je přece jenom menší šance, že by programátor udělal 2x podobnou chybu.

Ano, křížová kontrola, to jsem unittestům přiznal jako bod :-) To si moc nedovedu představit jak by se dělalo jinak. Ale třeba časem :-)

Ale k čemu je to dobré, když jednotkové testy můžete vytvořit v jakémkoliv jazyku bez potřeby doplnění syntaxe či preprocesoru, a to při větší vyjadřovací schopnosti, protože není třeba vytvářet nový (aťto deklarativní či imperativní) jazyk, ale stačí ten vlastní.

Viděl jsem spoustu testů. A nedomnívám se, že by to byl nějaký zázrak. Je to ukecané, nudlovité, neexpresivní, nedostatečné.

[gll]

A otázka zní, jaké to tedy má výhody? A dá se to napsat jinak? Typem?

funguje to se současnými technologiemi, nejen s nějakým sci-fi překladačem.

[v]

není jenom java a coq, výběr je větší a metod k potlačení chyb taky můžeme použíc víc než jednu (QuickCheck třeba ještě)

[SB]

není jenom java a coq, výběr je větší a metod k potlačení chyb taky můžeme použíc víc než jednu (QuickCheck třeba ještě)

O žádné konkrétní implementaci jsem nemluvil. Všechno jsou to jen variace na dané téma.

[JSH]

Ano, křížová kontrola, to jsem unittestům přiznal jako bod :-) To si moc nedovedu představit jak by se dělalo jinak. Ale třeba časem :-)

Možná tak v době, kdy si účetní pokecá s AI, přidá k tomu sbírku zákonů a ven vypadne hotový soft.

Seznam ukázkových příkladů je blízko neformálnímu popisu problému. Dokonce ho může dodat i klient s minimální představou o programování. Jakýkoliv typový systém je už o úroveň abstrakce dál. Takže i když už programátoři nebudou hrnout kód, ale jenom formální specifikace, tak budou testy užitečné.

[BoneFlute]

Seznam ukázkových příkladů je blízko neformálnímu popisu problému. ... Jakýkoliv typový systém je už o úroveň abstrakce dál. Takže i když už programátoři nebudou hrnout kód, ale jenom formální specifikace, tak budou testy užitečné.

Přijde mi zajímavější, aby ukázkové příklady generoval nástroj na základě specifikace. Včetně okamžiku vývoje.

Dokonce ho může dodat i klient s minimální představou o programování.

No já nevim. To už je otázka spíše psychologická. Veškeré mé zkušenosti s takto neznalími klienty bylo, že mi to museli vysvětlit ústně, protože sami jinak nehli prstem.

[BoneFlute]

A otázka zní, jaké to tedy má výhody? A dá se to napsat jinak? Typem?

funguje to se současnými technologiemi, nejen s nějakým sci-fi překladačem.

Dobře, máš pravdu. Ale vzhledem k námětu tohoto vlákna nás zajímá právě ten sci-fi překladač.
Takže, dá se to napsat jinak? Typem?