Zobrazit příspěvky
Tato sekce Vám umožňuje zobrazit všechny příspěvky tohoto uživatele. Prosím uvědomte si, že můžete vidět příspěvky pouze z oblastí Vám přístupných.
tak v tom případě by mohlo stačit i tohle ?To musi vedet ty, jestli by ti to stacilo
http://www.flajzar.cz/pristupove-systemy-rfid/ctecka-cipu-rfid-modul-id-10.htm
Pokud připustíte, že programování v jazyce Coq (nebo jiném podobném jazyce - např. Isabelle) je součást praxe, tak to odporuje vašemu tvrzení:Mluvil jsem samozrejme o problemu zastaveni realneho (cili omezeneho) pocitace. Cili napriklad problem zastaveni i386 s 1GB RAM. Myslel jsem, ze to je z kontextu dostatecne jasne.CitaceV PRAXI h.p. resitelny JE. A jde i naprosto trivialne dokazat, ze resitelny je.
Nic méně dál se tu píše 8bits + 1 ukončovací, takže by to ve finále asi stejně nešlo.Ma to pevne dany baudrate a format, jak pres uart komunikuje. To je problem?
Z ascii by to na HEX šlo, ale spíš potřeboval vidět co to přesně vyplivne za data a zkusit to.Vyplivne to hex id v ascii, takze dekodovat nejak takhle:
uint8_t hexdigit(uint8_t d) {
if (d>='0' and d<='9') return d-'0';
if (d>='A' and d<='F') return d-'A'+10;
return 0;
}
[...]
for(i=0;i<sizeof(id);i++) {
card[i] = (hexdigit(buff[i*2])*16) + hexdigit(buff[(i*2)+1]);
}Snažím se říct to, že při programování v určitých programovacích jazycích potřebujete dokázat, že funkce je totální pro všechny vstupy a nestačí to jen pro některé (což mj. znamená, že musíte dokázat, že na každém vstupu zastaví).Hm, to jsme radi, ze to vime. A jak to souvisi s tematem?
Taková skupina je i na MFF UK.Tak at nejsem pozadu: i na FI MU: http://www.fi.muni.cz/research/formal-methods/verification.xhtml.cs
Idea je: typy jsou tvrzení a funkce jsou jejich konstruktivní důkazy - bez totálnosti funkcí bych mohl dokázat cokoliv, neboť např. funkce, jenž nikdy nic nevrátí (cyklí), může mít libovolný typ (dokazuje libovolné tvrzení).No a co se tim snazis rict? Ze si umime vymyslet problemy, ktere nejsou ani teoreticky resitelne? To ale vsichni vime a nikdo to nerozporuje. Jenom to jaksi vubec nesouvisi s tim, o cem psal DK, a od ceho se tahle nova iterace stare debaty odpichla...
Jenže při verifikaci v Coqu potřebujete totálnost nad všemi vstupy - tj. řešit HP pro daný program na ničím neomezeném stroji. Netotální funkce vám totiž do logického systému Coqu vnáší spor a celá verifikace je k ničemu.Coq neznam, takze konkretne nemuzu rict, ale obecne u takovychto problemu jde o to, ze jsou to prave problemy zadane tak, ze nejsou nicim omezene. A ta neresitelnost primo plyne prave z te neomezenosti.
Třeba při verifikaci programů v Coqu potřebujete garantovat totálnost funkcí - tj. potřebujete provést důkaz terminace. Tam HP řešitelný není.Jeste jednou: pokud mam abstraktni program pro abstraktni, nicim neomezeny stroj, tak HP ani teoreticky resitelny neni. Pokud mam realny program pro realny stroj, tak HP teoreticky resitelny je. Vzdy a dokazatelne. Jak je to prakticky, to uz je jina otazka.
Hlavně to (obecně) nelze ověřit na tom samém stroji.Jasne, ale pak si taky musime rict, co znamena slovo "obecne". To znamena "bez dalsich omezujicich podminek". A takove problemy proste v realu resit nepotrebujes.
Neshodli jsme se tu na tom, že HP v praxi řešitelný je, ale navržené řešení je v praxi nepoužitelnéNe. Shodli jsme se (doufam) na tom, ze k reseni konkretniho zastaveni konkretniho algoritmu "narocnosti" N je potreba algoritmus "narocnosti" nejake f(N). Prakticka pouzitelnost nebo nepouzitelnost pak je dana porovnanim velikosti f(N) s tim, co mam realne k dispozici k reseni naseho realneho problemu.
jednoduse proto, ze to "ma ve voku", a i kdyz to neumi spocitat/dokazat/... tak "vi", ze to reseni je OK.Ale on to ani ten teoretik neumi "spocitat" a "dokazat". Korektne dokazat jdou vicemene jenom abstraktni (->zjednodusene, zidealizovane) problemy. Nikdo ti nikdy nedokaze, jestli je pro firmu X vyhodnejsi pouzit jako wifi AP Mikrotik nebo Ubiquity nebo jestli je lepsi nasadit NFS nad ufs nebo zfs. To je proste expertni znalost/zkusenost, ziskana lety praxe a milionkrat opakovanymi zkusenostmi. A takovehodle typu je drtiva vetsina SKUTECNYCH problemu v IT. "Teorie", ktera je v REALNEM IT skutecne potreba je typu ITIL, ne typu Turing, at si kdo chce co chce rika a at si ded kenedy povazuje za idiota treba cely svet.
Zase, kolik lidi pise prekladace? Potrebuje bezny programator umet psat prekladac?Ale jo, obcas podobne veci potrebuje. Treba si chce vytvorit nejaky vlastni datovy format a chce k nemu napsat parser. Nebo treba chce parsovat YAML v Erlangu a zjistil, ze na to neni zadna dost dobre napsana knihovna.
Vis, problem je v tom, ze na VS se vytvori umely problem, a kolem nej se pak teoretizuje, misto aby se vzala realna uloha, a na ni se ukazalo jak ji lze resit a proc.No jo, tomu se rika veda
A problem je v tom, ze mnoho VS se ze vsech abslventu snazi delat polo-vedce, coz je zbytecne, protoze ve vede stejne nikdy pracovat nechteji a nebudou.A vubec nejlepsi na tom je, ze spousta programatoru prekladacu tu teorii kolem vubec nezna ..Ne. Nejlepsi na tom je to, ze tu teorii neznaji ti, kdo se jeji znalosti ohaneji - s dead kenedym a JS v cele.
Ty už zase piješ ten Marihuanový JIN?Jedině Jang!
Root.cz (www.root.cz), informace nejen ze světa Linuxu. ISSN 1212-8309
Copyright © 1998 – 2023 Internet Info, s.r.o. Všechna práva vyhrazena. Powered by Linux.
