Typový system versus unittesty

Kit

Re:Typový system versus unittesty
« Odpověď #600 kdy: 29. 06. 2018, 09:57:50 »
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á.
Citace
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?


SB

Re:Typový system versus unittesty
« Odpověď #601 kdy: 29. 06. 2018, 10:04:45 »
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

Re:Typový system versus unittesty
« Odpověď #602 kdy: 29. 06. 2018, 11:08:58 »
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á.
Citace
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

Re:Typový system versus unittesty
« Odpověď #603 kdy: 29. 06. 2018, 11:42:12 »
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ě.

Re:Typový system versus unittesty
« Odpověď #604 kdy: 29. 06. 2018, 11:57:52 »
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).


JSH

Re:Typový system versus unittesty
« Odpověď #605 kdy: 29. 06. 2018, 11:58:38 »
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

Re:Typový system versus unittesty
« Odpověď #606 kdy: 29. 06. 2018, 12:05:08 »
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

Re:Typový system versus unittesty
« Odpověď #607 kdy: 29. 06. 2018, 13:30:08 »
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

  • *****
  • 1 844
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #608 kdy: 29. 06. 2018, 14:16:28 »
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

  • ****
  • 429
    • Zobrazit profil
    • E-mail
Re:Typový system versus unittesty
« Odpověď #609 kdy: 29. 06. 2018, 14:39:09 »
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

Re:Typový system versus unittesty
« Odpověď #610 kdy: 29. 06. 2018, 14:50:28 »
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

Re:Typový system versus unittesty
« Odpověď #611 kdy: 29. 06. 2018, 15:02:08 »
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

Re:Typový system versus unittesty
« Odpověď #612 kdy: 29. 06. 2018, 15:56:09 »
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

  • *****
  • 1 844
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #613 kdy: 29. 06. 2018, 16:11:09 »
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

  • *****
  • 1 844
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #614 kdy: 29. 06. 2018, 16:12:31 »
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?