Typový system versus unittesty

[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.

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ý.

Myslim, ze u rady problemu je overeni spravnosti vypoctu trivialni kdezto vypocet samotny je slozity.
A kdyz zakomponuju overeni spravnosti do konstrukce navratoveho typu zarucim tim ze nepujde vytvorit navratovy typ obsahujici nespravny vysledek.

Ano je to v podstate znovuimplementace jinak, a da se v tom taky udelat chyba, ale pokud je to overeni opravdu radove jednodussi dava mi to vetsi smysl, nez napsat par testu rucne.


 

[Reklama]

[Filip Jirsák]

Myslim, ze u rady problemu je overeni spravnosti vypoctu trivialni kdezto vypocet samotny je slozity.
A kdyz zakomponuju overeni spravnosti do konstrukce navratoveho typu zarucim tim ze nepujde vytvorit navratovy typ obsahujici nespravny vysledek.

Jistě existuje řada takových problémů, ale podle mne se to netýká drtivé většiny problémů řešených dnešními programy. Navíc to ověření správnosti zabere nějaký výkon za běhu – lepší je (obvykle) ověřit správnost v době vytváření programu a za běhu se už jen spoléhat na to, že to prostě je správně.

[hawran diskuse]

....
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.

+1
(obdivuji Tvou trpělivost)

[hawran diskuse]

...
A kdyz zakomponuju overeni spravnosti do konstrukce navratoveho typu zarucim tim ze nepujde vytvorit navratovy typ obsahujici nespravny vysledek.

Huh?

Ano je to v podstate znovuimplementace jinak, ...

Asi tak.

[gll]

Tak já se obecně domnívám, že ruční psaní unittestů je jen mezistupeň a v budocnosti to nahradí automatika.

nebo automatika nahradí psaní programů a zůstane jen psaní testů (generování testových dat), ze kterých se budou učit neuronové sítě.

[Reklama]

[BoneFlute]

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.

Což je cíl, ke kterému směřujeme.

[BoneFlute]

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".

Nutno zopakovat, že to, že došlo k prohození "a" a "b" se v Typu neopodchytí, stejně jako se nepodchytí toto prohození v Unittestech. Tudíž vzhledem k námětu tohoto vlákna je tento dotaz irelevantní.

[andy]

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ů.

Nějak jsem nepochopil, co to má společného s tím, že když naučíme compiler pracovat se symbolickou matematikou, tak pro něj není problém odvodit, že standardní řešení kvadratické rovnice splňuje specifikace požadovanou po té funkci. Je to asi tak na stejné úrovni, jako že ten Liquid haskell je pro (některé) programy schopen dovodit, že výsledkem funkce je neprázdné pole.

Takže reakce na tebe:

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

Kompilátor, který neví nic o kvadratických rovnicích, ale umí pracovat s matematickými výrazy (nepovažoval bych za vyloučené, že by tím směrem ty idrisy a spol. ohnout šly), je schopen dokázat, že daná funkce tu kvadratickou rovnici řeší.

[Kit]

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".

Nutno zopakovat, že to, že došlo k prohození "a" a "b" se v Typu neopodchytí, stejně jako se nepodchytí toto prohození v Unittestech. Tudíž vzhledem k námětu tohoto vlákna je tento dotaz irelevantní.

Jednotkové testy to právě odhalí velmi rychle už při odečítání.

[BoneFlute]

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".

Nutno zopakovat, že to, že došlo k prohození "a" a "b" se v Typu neopodchytí, stejně jako se nepodchytí toto prohození v Unittestech. Tudíž vzhledem k námětu tohoto vlákna je tento dotaz irelevantní.

Jednotkové testy to právě odhalí velmi rychle už při odečítání.

Narážíš-li na komutativitu, tak tímto způsobem to zase odhalí i Typ.

[Kit]

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".

Nutno zopakovat, že to, že došlo k prohození "a" a "b" se v Typu neopodchytí, stejně jako se nepodchytí toto prohození v Unittestech. Tudíž vzhledem k námětu tohoto vlákna je tento dotaz irelevantní.

Jednotkové testy to právě odhalí velmi rychle už při odečítání.

Narážíš-li na komutativitu, tak tímto způsobem to zase odhalí i Typ.

Jak ten typ bude vypadat?

[listoper]

Myslim, ze u rady problemu je overeni spravnosti vypoctu trivialni kdezto vypocet samotny je slozity.
A kdyz zakomponuju overeni spravnosti do konstrukce navratoveho typu zarucim tim ze nepujde vytvorit navratovy typ obsahujici nespravny vysledek.

Jistě existuje řada takových problémů, ale podle mne se to netýká drtivé většiny problémů řešených dnešními programy. Navíc to ověření správnosti zabere nějaký výkon za běhu – lepší je (obvykle) ověřit správnost v době vytváření programu a za běhu se už jen spoléhat na to, že to prostě je správně.

Ten prispevek je prece o generativnim testovani u dynamicky typovaneho jazyka.
Za behu prece nebudu zapinat "typovou" instrumentaci.

[BoneFlute]

Narážíš-li na komutativitu, tak tímto způsobem to zase odhalí i Typ.

Jak ten typ bude vypadat?

Přiznávám se bez mučení, že zde mé znalosti končí. Ale mám rámcovou představu, jak by to mělo jít: pokud vím, že operátor sčítání je, a operátor odčítání není komutativní, tak IMHO není problém to kompilátoru říct. Jak konkrétně by se to zapsalo, to netuším. Mám toho ještě hodně k nastudování.

[Filip Jirsák]

Nějak jsem nepochopil, co to má společného s tím, že když naučíme compiler pracovat se symbolickou matematikou, tak pro něj není problém odvodit, že standardní řešení kvadratické rovnice splňuje specifikace požadovanou po té funkci. Je to asi tak na stejné úrovni, jako že ten Liquid haskell je pro (některé) programy schopen dovodit, že výsledkem funkce je neprázdné pole.

Jenom jsem upřesnil, že to, co popisujete, je jenom vytčení něčeho jednoduchého do knihovny nebo kompilátoru, které pak jako programátor používáte už bez testování. To ale není nic nového. Takhle už máte něco implementováno třeba v C kompilátoru nebo standardní knihovně – a ty implementace se zase testují.

Kompilátor, který neví nic o kvadratických rovnicích, ale umí pracovat s matematickými výrazy (nepovažoval bych za vyloučené, že by tím směrem ty idrisy a spol. ohnout šly), je schopen dokázat, že daná funkce tu kvadratickou rovnici řeší.

Ne, kompilátor není schopen dokázat, že daná funkce řeší kvadratickou rovnici. Kompilátor je schopen dokázat, že daná funkce řeší něco, co programátor prohlašuje za kvadratickou rovnici.

[Filip Jirsák]

Ten prispevek je prece o generativnim testovani u dynamicky typovaneho jazyka.
Za behu prece nebudu zapinat "typovou" instrumentaci.

Jak zakomponujete ověření správnosti výsledku do konstukce návratového typu, aby se to ověření nedělalo až za běhu, ale už při překladu?