Typový system versus unittesty

Re:Typový system versus unittesty
« Odpověď #420 kdy: 26. 06. 2018, 11:21:32 »
mj. jsem narážel na to vaše "sebelepší typový systém nemůže..."
To ale není odmítání moderních technologií nýbrž pouhé konstatování faktu. Když mne někdo bude přesvědčovat, že má vymyšlený stroj, do kterého nemusí vkládat žádnou energii a ten stroj jí vyrábí, a že už mu to skoro funguje, jenom ještě dořeší nějaké detaily, odmítnu to. Ne proto, že bych odmítal moderní technologie, ale proto, že podle současného stavu poznání perpetuum mobile nelze vyrobit.


v

Re:Typový system versus unittesty
« Odpověď #421 kdy: 26. 06. 2018, 11:23:10 »
mj. jsem narážel na to vaše "sebelepší typový systém nemůže..."
To ale není odmítání moderních technologií nýbrž pouhé konstatování faktu. Když mne někdo bude přesvědčovat, že má vymyšlený stroj, do kterého nemusí vkládat žádnou energii a ten stroj jí vyrábí, a že už mu to skoro funguje, jenom ještě dořeší nějaké detaily, odmítnu to. Ne proto, že bych odmítal moderní technologie, ale proto, že podle současného stavu poznání perpetuum mobile nelze vyrobit.
a jste si jistý, že ten současný stav poznání máte podchycený? teď narážím na "dependent types"

netypová lopata

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

SB

Re:Typový system versus unittesty
« Odpověď #423 kdy: 26. 06. 2018, 11:53:39 »
...Stoprocentní pokrytí kódu testy znamená, že se při testech projdou všechny „řádky“ (ve skutečnosti instrukce) programu...

Toto je chybné tvrzení. Vy sám jste napsal, že testy nesmějí obsahovat algoritmus, neboli duplikovat implementaci. Úkolem testů není ověření samotné implementace, ale ověření správnosti výstupů pro všechny kombinace možných vstupů, to je 100% pokrytí testem. To je ale obvykle nereálné, takže alespoň jejich části.
To spolu ale nesouvisí. Testy mohou pokrývat 100 % kódu, tj. při spuštění testů se spustí všechny instrukce kódu. To ale vůbec neznamená, že by test duplikoval implementaci. Za „pokrytí testy“ se obvykle označuje právě poměr počtu instrukcí procházených při testech k celkovému počtu instrukcí knihovny či aplikace, protože to se dá změřit. To je reálné (i když to nemusí být nutné, protože chybějící testy mohou nepokrývat nezajímavé části kódu), ale v žádném případě to neříká, že by se testovaly všechny možné vstupy, nebo že by program byl bezchybný, pokud testy projdou. Ukazatel „pokrytí kódu/řádků/instrukcí testy“ má opačný význam – pokud určitá větev programu není testem pokrytá, víme určitě, že pomocí testů určitě nedokážeme poznat, zda v dané části chyba je nebo není.

To se mi nějak nezdá - 100% pokrytím někteří myslí pokrytí celého protokolu objektu, tj. viditelných metod. Že testy nespustí některý vnitřní kód, nemusí znamenat vůbec nic, např. část kódu je nevyužitá (např. před refaktorizací). Nebo si představte, že vytvoříte testy cizí knihovny, do které vůbec nevidíte.

SB

Re:Typový system versus unittesty
« Odpověď #424 kdy: 26. 06. 2018, 12:07:56 »
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:

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

Phi má recht, obecně to nejde, ale ve speciálních (neřešíme ale, jak často!) ano:

class Vědma:
    odpověďNaOtázkuŽivota():
        return 42

testVědmy:
    assert(Vědma().odpověďNaOtázkuŽivota() == 42)

A je to pokryto. Důkaz sporem.


netypová lopata

Re:Typový system versus unittesty
« Odpověď #425 kdy: 26. 06. 2018, 12:24:08 »
Phi má recht, obecně to nejde, ale ve speciálních (neřešíme ale, jak často!) ano:

Já ale řeším, jak často. Je hezké, že jsi z nekonečného prostoru možných programů vytáhl jeden (který je mimochodem úplně k ničemu), na kterém něco prokážeš. Praktický přínos je nicméně nulový. Pro každý netriviální běžný program, který něco rozumného dělá, tvoje metoda selže. Lidé obvykle chtějí otestovat bežné programy, které mají nějaký užitek. A to neumíme, nedokážeme říct se 100% jistotou, že je program správný, nemáme na to metodu.

Kit

Re:Typový system versus unittesty
« Odpověď #426 kdy: 26. 06. 2018, 12:28:00 »
předpokládejme tu vaši specifikaci ("sečte hodnoty parametrů") a zahoďme moji funkci, jak budou vypadat testy?

Tak především se test nekouká dovnitř, ale zvenčí. A kouká se jen na vlastnosti, které jsou od té funkce požadovány. Pokud je požadavkem "sečíst hodnotu numerických parametrů", tak obvykle stačí třeba:
Kód: [Vybrat]
def testX():
    assert(x(3, 5) == 8)
    assert(x(-3, 5) == 2)
    assert(x(3, -5) == -2)
    assert(x(-3, -5) == -8)

Pokud nebudu mít na vstupu např. záporná čísla, mohu odpovídající testy vypustit. Pokud budu chtít touto funkcí spojvat i řetězce nebo posouvat čas o offset, tak je do testu přidám. Pokud potřebuji, aby funkce při výsledku nad hodnotu 100 vyhodila výjimku nebo ten výsledek ořízla (např. životy u her), tak tam takový test také přidám. Dříve definovaná funkce tím přestane procházet a vývojář ji musí upravit.

Tímto způsobem mohu testovat i cizí knihovny, do kterých nevidím, ale očekávám od nich určité chování pro různé očekávané i méně očekávané vstupy. Pokud její autor změní něco, co bude mít vliv na moji aplikaci, dozvím se to.

Re:Typový system versus unittesty
« Odpověď #427 kdy: 26. 06. 2018, 12:28:11 »
Tak bych si dovolil tvrdit, že programátora v jazyce s ADT null pointer exception chybu řešit fakt napadne, protože tam jinak ten "null" nedostane, zatímco u assertu toho programátor fakt mnohokrát nenapadne tam ten assert vůbec dát.
To záleží na kontextu. Pokud se bude pohybovat v kódu, kde bude většina typů non-null, a výjimečně narazí na nullable typ, ošetří to. Pokud bude z venku neustále dostávat nullable typy a použité typy a typový systém ho budou nutit neustále to přetypovávat, bude to dělat automaticky bez přemýšlení.

Takže bych to upřesnil, že komplexnější typový systém sám o sobě nic nezaručuje, pouze dává větší možnosti. A je na jeho uživatelích, zda ty možnosti využijí – přičemž je potřeba počítat i s tím, že (i podle typů projektů) je různá úroveň programátorů, a nedá se počítat s tím, že ty miliony webových aplikací budou programovat lidé, kteří budou důsledně používat složitý typový systém – bylo by to příliš drahé. Je ale dobré, když se podaří (jako to má třeba Google) využít typový systém v důležitých částech tak, že ty typy nadefinují specialisté, a řádový programátor pak už jen používá typy „obyčejný text“ (který nemůže do HTML vypsat jinak, než escapovaně), a typ „HTML text“, který se při výstupu do HTML neescapuje, ale zase v něm není možné vytvořit nebezpečnou HTML konstrukci (např. náchylnou na XSS).

Takže konkrétně nullpointerexception mi připadá jako protipříklad Tvého tvrzení, a nepřipadá mi, že by cokoliv, co jsi napsal poté (byť třeba s tím odstavcem výše souhlasím) jakkoliv tu ideu, že typový systém a unit testy jsou srovnatelné, protože v obojím může udělat programátor chybu, podporovalo.
Já ale netvrdím, že typový systém a jednotkové testy jsou srovnatelné. Tvrdím, že naopak každý řeší něco jiného, takže obecně nejsou navzájem nahraditelné – i když existuje určitá oblast, kterou je možné řešit oběma způsoby, a když používáte slabší typy, je vhodné danou oblast kontrolovat pomocí jednotkových testů. Jako v tom příkladu s XSS – kdo nepoužívá typy pro bezpečné HTML, jako Google, měl by mít alespoň jednotkové testy snažící se XSS odhalit (což je zrovna dost obtížné a podle mne je snazší řešit to pomocí těch typů).

Kit

Re:Typový system versus unittesty
« Odpověď #428 kdy: 26. 06. 2018, 12:31:27 »
Phi má recht, obecně to nejde, ale ve speciálních (neřešíme ale, jak často!) ano:

Já ale řeším, jak často. Je hezké, že jsi z nekonečného prostoru možných programů vytáhl jeden (který je mimochodem úplně k ničemu), na kterém něco prokážeš. Praktický přínos je nicméně nulový. Pro každý netriviální běžný program, který něco rozumného dělá, tvoje metoda selže. Lidé obvykle chtějí otestovat bežné programy, které mají nějaký užitek. A to neumíme, nedokážeme říct se 100% jistotou, že je program správný, nemáme na to metodu.

Zrovna kontrola, zda mají externí konstanty jednotky správné hodnoty, do testů patří.

Re:Typový system versus unittesty
« Odpověď #429 kdy: 26. 06. 2018, 12:33:16 »
To se mi nějak nezdá - 100% pokrytím někteří myslí pokrytí celého protokolu objektu, tj. viditelných metod. Že testy nespustí některý vnitřní kód, nemusí znamenat vůbec nic, např. část kódu je nevyužitá (např. před refaktorizací). Nebo si představte, že vytvoříte testy cizí knihovny, do které vůbec nevidíte.
Pokrytí všech instrukcí kódu je to jediné, co se dá relativně snadno změřit, proto to bývá jedna z metrik, které se měří při sestavení projektu. Takže když na nějakém výstupu (třeba od https://codecov.io/) uvidíte metriku „pokrytí testy“, je to právě tohle. Jinak samozřejmě „pokrytí testy“ může znamenat i ledacos jiného, pak by ale každý, kdo to spojení použije, měl uvést, co tím vlastně myslím. Jinak to dopadne jako tady, kde se několik lidí hádá o pokrytí testy, a přitom tím každý myslí něco jiného.

Re:Typový system versus unittesty
« Odpověď #430 kdy: 26. 06. 2018, 12:35:20 »
Chápu správně, že tvá definice "100% pokrytí" == "kód pracuje správně"?
Je snad jiná definice 100% pokrytí testy? Pokud se test tváří, že pokrývá nějakou vlastnost, ale ve skutečnosti nedělá nic, tak do této statistiky nemůže být zahrnut.
Pokud definuješ 100% pokrytí testy jako "kód pracuje správně", tak pak tvoje rada zní "pište programy správně"...

Zajímavá implikace. Na to jsi přišel matematickými postupy?

Pokud testy prochází a program přitom nepracuje správně, nemohu tvrdit, že má 100% pokrytí testy.

Samozreme, ze muzes. Pokryti testy je jedna metrika, kvalita tech testu vec jina...

Re:Typový system versus unittesty
« Odpověď #431 kdy: 26. 06. 2018, 12:51:08 »
a jste si jistý, že ten současný stav poznání máte podchycený? teď narážím na "dependent types"
Ano, jsem si tím jistý.

V různých dobách se perpetua mobile vytvářejí na základě v té době moderních věcí – někdy to byl „magnétismus“, někdy „paprsky X“, jindy „elektřina“, dneska to často budou „kvantové jevy“, „energie vakua“ nebo nejnověji nejspíš „temná hmota“. Což nic nemění na tom, že nemožnost konstrukce perpetua mobile plyne z fundamentálních zákonů, a nemusíme znát detailní fungování temné hmoty, nemusíme mít sjednocenou teorii gravitace a kvantové teorie, nemusíme tušit, co se ve fyzice objeví za padesát nebo za sto let, pořád si ale můžeme býti dost jistí, že ani pak nepůjde zkonstruovat perpetuum mobile.

Stejně tak si můžeme být dost jistí, že nepůjde mechanicky zkontrolovat, zda program bude fungovat správně – například i proto, že „správné fungování“ je subjektivní věc, a co může být v jednom případě považováno za správné fungování, v jiném případě tak být nemusí.

Pak je podstatná ještě jedna věc, která tu zatím moc nebyla zmíněna, a to je to, že typový systém může něco užitečného přinést jedině tehdy, když se používá, tedy když ho programátoři chtějí používat. Stačí se podívat na takové malinké vylepšení hloupého typového systému Javy, jakým jsou kontrolované výjimky. Ani tohle drobné typové omezení se prakticky neujalo, a to je velmi jednoduché kontrolované výjimky jak definovat, tak používat. I to připadá většině Java vývojářů jako zbytečně moc práce v porovnání s jejím přínosem. Takže navrhovat nové typy pro masové použití klidně můžete, ale pak se vám také klidně může stát, že budou vznikat a široce se používat knihovny, které budou jako jednu ze svých důležitých vlastností uvádět to, že ruší ten váš typový systém.

andy

Re:Typový system versus unittesty
« Odpověď #432 kdy: 26. 06. 2018, 13:18:15 »
Tak bych si dovolil tvrdit, že programátora v jazyce s ADT null pointer exception chybu řešit fakt napadne, protože tam jinak ten "null" nedostane, zatímco u assertu toho programátor fakt mnohokrát nenapadne tam ten assert vůbec dát.
To záleží na kontextu. Pokud se bude pohybovat v kódu, kde bude většina typů non-null, a výjimečně narazí na nullable typ, ošetří to. Pokud bude z venku neustále dostávat nullable typy a použité typy a typový systém ho budou nutit neustále to přetypovávat, bude to dělat automaticky bez přemýšlení.
Ano, a to jsem přesně měl na mysli, když jsem říkal, že typ Maybe není totéž co assert. Ukázka (ne-generického) dekódování JSONu s non-null a jedním nullable typem ..
Kód: [Vybrat]
data Obj {
    a :: Int
  , b :: Text
  , c :: [Int]
  , d :: NonEmpty Int -- neprazdne pole
  , e :: Maybe Double
  , f :: UTCTime
}
instance FromJSON Obj where
  parseJSON = withObject $ \o ->
     Obj <$> o .: "alpha" <*> o .: "beta" <*> o .: "cyril" <*> o .: "delta" <*> o .: "edward" <*> f .: "ftime"
Máš pravdu, když to píšu, tak to píšu bez přemýšlení... až na to, že tohle je kód, který je dost důsledně kontroluje, jestli ve zdrojových datech nechybí atributy, jestli to pole "delta" je fakt neprázdné, jestli tam někde nejsou nully.... a teď mi řekni, jak bys to psal v dynamickém jazyku a jak by vypadaly unit testy....

Jinak pokud jde o XSS, tak bych neřekl, že je to principálně věc typů.

v

Re:Typový system versus unittesty
« Odpověď #433 kdy: 26. 06. 2018, 13:22:34 »
a jste si jistý, že ten současný stav poznání máte podchycený? teď narážím na "dependent types"
Ano, jsem si tím jistý.
z jakých materiálů jste čerpal? popř. v jakém jazyce jste to zkoušel?

andy

Re:Typový system versus unittesty
« Odpověď #434 kdy: 26. 06. 2018, 13:23:11 »
Citace: andy
Jinak pokud jde o XSS, tak bych neřekl, že je to principálně věc typů.
Beru zpět, ano XSS jde řešit typy a zrovna docela hezky.