Začínáme si „nebezpečně“ zvykat na myšlenku, že počítačový program nemusí vždy pracovat správně. Zatímco poruchové auto vrátíme zpátky prodejci a požadujeme nápravu, v otázce poruchovosti počítačových programů jsme pozoruhodně tolerantní.
Program, který kupujeme, je obvykle bez záruky a nechvalně známé „zřeknutí se odpovědnosti“ je všechny provází, jako nedílná součást instalačního manuálu. Snad už ani nikdo neočekává, že všechno bude fungovat správně, jakmile se to jednou vybalí „z krabice“. A co je snad nejhorší, neočekává to ani sám výrobce. Ve skutečnosti to většinou vypadá tak, že firmy vyvíjející a prodávající software spoléhají na to, že jejich zákazníci objeví chyby, které pak mohou „zalepit“ vydáním „upgradu“ produktu.
Nordström si myslí, že celý přístup k psaní programů by měl být přehodnocen. Obvyklý přístup spočívá v ověření správnosti fungování programu prostřednictvím dlouhého testovacího procesu. Namísto toho bychom rádi viděli návrh základního principu, který zaručí, že od „první věty“ bude program opravdu dělat to, co se od něj očekává a co je napsáno na krabici v které ho koupíte.
Klíč k tomuto problému leží v těžko srozumitelných matematických formulacích, které popisuje takzvaná „teorie modelu“ založená na teorii výpočtu. V tomto přístupu je specifikace pro výpočetní úlohu uvedená jako matematický teorém. Program, který provádí výpočet, je obdobou prokázání teorému. Ověřením tohoto teorému je zaručeno, že program bude v pořádku.
Otevřený zdrojový kód programu
Samozřejmě, že to není tak jednoduché, ale teorie modelu je tak slibnou možností, že Evropská unie již od roku 1989 financuje celý řetězec projektů k jejímu vývoji, pod záštitou programu Future and Emerging Technologies.
Nordström byl koordinátorem jednoho z projektů, nazvaného TYPES, který podporoval spolupráci výzkumníků zabývajících se touto problematikou na 15 evropských univerzitách a výzkumných ústavech společně s těmi v 19 vědeckých a průmyslových organizacích.
Partneři projektu TYPES také vydávají otevřené zdrojové programové balíky, které si může kdokoliv stáhnout, použít a upravit. Tyto balíky obsahují několik „testovacích editorů“, které jsou v teorii modelu klíčem k zaručení správnosti programů.
Může takový abstraktní teoretický výzkum opravdu vést k bezporuchovému softwaru?
„Evropský výzkum v této oblasti je nejsilnějším na světě,“ zdůrazňuje Nordström. „Mnoho počítačových programů pracuje špatně nebo nepracuje odpovídajícím způsobem a v dlouhodobém časovém horizontu může být tento výzkum skutečně významným pomocníkem. Jde o velmi pomalý proces a zabere to spoustu let, než dostaneme tento nápad z univerzit do „provozu“, ale myslím si, že už si zde pomalu nachází své místo.“
„Princip otevřeného zdroje je nezbytný pro to, čeho se pokoušíme dosáhnout,“ říká Nordström. „Je důležité, aby kdokoliv mohl vyhodnotit tento zdrojový kód a zkontrolovat, jestli je správný. Takže neodmyslitelnou součástí tohoto projektu by mělo být, že cokoliv v programu uděláme, bude přístupné i ostatním, aby se o tom mohlo následně diskutovat.“
Výsledky z teorie modelu si již našly svou cestu do jiných projektů. Příkladem může být projekt Moebius, financovaný Evropskou unií, který vyvíjí nové metody, tak zvané „testovací kódy“, jejichž účelem bude ověřovat bezchybnost stahovatelných programů.
Jedna francouzská společnost využívá myšlenky z teorie modelu k návrhům napevno nainstalovaných počítačových programů, jaké jsou například používané v „chytrých kartách“. A ani Japonsko nezůstává v této oblasti výzkumu pozadu.
Teorie v praxi
Výzkumníci také předvedli schopnosti teorie modelu prověřením klasického teorému „čtyř barev“ jedním z testovacích editorů používáných v projektu TYPES. Ale teorie modelu také nachází uplatnění i v jazykových analýzách.
Nordström se nedomnívá, že by využití teorie modelu bylo nezbytné pro všechny programy, ale je zcela jasné, že bude potřeba například pro zabezpečení rozhodujících bankovních systémů. Krom toho by teorie modelu mohla být důležitou též v oblastech dopravy, obrany a zdravotnictví, kde může být za chyby v programech placeno lidskými životy.
TYPES obdržel finance od Evropské unie z programu Sixth Framework Programme pro výzkum spočívající v „koordinační činnosti“ popisující projekty, jejichž cílem je spíš „promazávat soukolí“ spolupráce, než přímo vyvíjet novou technologii. TYPES spojuje základní a aplikovaný výzkum. „To je jedna z věcí, kterou na této práci shledávám velmi zajímavou v porovnání s ostatními vědními obory,“ poznamenává Nordström. „Je nás celkem asi 150 lidí, kteří pracují na tomto projektu a je to směsice velmi praktických osob s velmi teoreticky orientovanými lidmi a mnoho si toho vzájemně poskytujeme. Myslím si, že je to velmi vzácné v porovnání s ostatními vědeckými projekty.“
Nordström doufá, že tato práce vykonaná v rámci projektu TYPES konečně umožní programování „dozrát“ do skutečně technické disciplíny se stejně vysokými standardy a zárukou kvality, jakou nyní očekáváme v kterémkoliv jiném technickém oboru.
„Mnoho úsilí je nyní věnováno testování softwaru,“ říká. „Velmi často jsou programy napsány ve spěchu, a pak jsou testovány a opravovány… a opět testovány a opravovány… a tak pořád dokola. To je strašně nesystematické. Není to ani vzdáleně podobné tomu, jak na příklad budujeme mosty a dálnice. Tento způsob práce nás připravuje na změnu tak, abychom více úsilí věnovali vlastnímu psaní programů, než jejich testování a opravování.“
Zdroj: ICT Results
Diskuze:
Metry a stopy
Honza Honza2,2008-07-28 08:28:44
Nejen metry a stopy. Třeba u rakety Ariane 5 dosáhlo při prvním startu zrychlení tak "obrovské" hodnoty, že přelezlo hranici 16 bitové integeru :-) Spadnul program ovládající inerciální plošiny, řídící počítač si nesmysly co mu dávala inerciální plošina přebral po svém a pokusil se s 700 tunovou raketou o ostrou pravou zatáčku :-) Bohužel to nevybral a kromě fungl nové rakety odepsal náklad čtyř družic na výzkum slunečního větru za půl mld. doláčů.
typ
Dominik Šefl,2008-12-12 23:52:10
často je opravdu problém s určitostí velikosti některých typů,myslím že by bylo spíše vhodné zevidovat způsob jakým počítače fungují,když mozek je pořád nejrychlejším počítačem. Už to snad vypadá že 3D architekturu nebudeme mít ani za 1000 let. A jsou i otravnější chyby než 1xročně pád Windows kvůli přetížení. Existují hry a software mezi sebou nekompatibilní a často se nezjistí vůbec který z běžících programů způsobí chybu nebo zmrznutí jiného.
Mě by stačilo kdyby hry běžely nezávisle na okolním softu a záleželo jen na HW. dokud se to nestane je pořád důvod vydávat na konzole.
Miro Hrazsky,2008-07-26 01:42:35
klasicka ukazka ako sa daju v socializme vyzierat spolocne prachy, nic viac.
Programy bez chyb
Honza Honza2,2008-07-25 10:32:15
Programy budou bez chyb až budou auta, ledničky a pračky bez poruch a boty z tržnice přežijou první vlhko. :-)
Nějaké vylepšení v kontrole programů by ale určitě bodlo. Nedávno jsem v jednom renomovaném statisickém programu narazil na to, že 6 / 2 = 3.00001. To se nezdá jako zas tak zásadní problém. Ale jenom dokud na všechny klienty, kterým vyjde hodnocení >3 nepošlete exekutora :-)
Počet katastrof způsobených špatným softwarem při letech do kosmu je taky na pováženou.
rychlost
Sam Hall,2008-07-24 19:05:44
Nakolik nový přístup urychlí a slevní vývoj aplikací?
Nejsou formální revize kódu alá Steve McConnell dostačující?
Tomáš Skopal,2008-07-24 20:27:17
McConell napsal Code Complete? To je spíš o technikách a metodikách, než o formálním důkazu...
Jinak - no nezrychlí se ani nezlevní. To je pokus o absolutni přesnost. Což je nesmysl, 100% bezchybnost stejně nejsou schopni garantovat (i když jí třeba dosáhnou, u 1+1=2 to jde ověřit snadno, ale jak to ověříte u milionu řádků heuristických algoritmů).
Celé je to o kompromisu - chcete mít 99% spolehlivost za $1000, nebo 99.9% za $10000? Jistě jsou případy, kdy je bezchybnost kritická, třeba letadla, roboti operující lidi, vysoká pec apod. Ale u textovýho editoru, kterej zálohuje co minutu text, je vám asi šumák, že třeba jednou za rok spadne... Asi je to lepší, než zaplatit 100x tolik za 2x lepší bezchybnost...
:)
Peca Pospec,2008-07-24 12:41:32
Tak hlavně, že je snaha :) Třeba při tom vymyslí mašinu, která toho zvládne víc než Turing a budem na ní verifikovat normální počítače :D
Tomáš Skopal,2008-07-24 13:12:27
no bohužel ani teoretický Turing nerozhodne, natož něco praktického... to je prostě klasický problém slepice-vejce, jenom posunutý jinam...
Pokud určitý program má dělat něco jiného, než už dělá nějaký jiný program, musí se holt tato nová informace nějak netriviálně popsat. Ať děláte co děláte, tu informaci/nápad prostě musíte zhmotnit. Kdyby to tak nebylo, vyrábíte něco, co už je, tudíž je to zbytečné... A i když jen lepíte existující programy, aby se vytvořil program nový, tak ono "lepení" (třeba používání knihoven) zase obsahuje tu novou informaci... Samozřejmě se mohou vymyslet mechanismy, aby se stejné chyby neopakovaly, např. tupá syntaktická kontrola překladače odchytí ty největší ptákoviny. Jenže čím je potenciální chyba víc sémantická, tím hůř je rozpoznatelná... když uděláte program, který počítá nějaký vzoreček, jak má překladač vědět, že se tam někde má něco přičítat místo násobit?? Ok, řeknete, pozná to tak, že ví ten vzoreček, přes kterej to kontroluje... no jo, ale ten vzoreček tam musíte naťukat. Takto se prostě celý ten proces mechanicky akorát zesložití, programátor přestane rozumět jádru, protože ta režie kolem ho odstaví od čistého kódu. Jediná rada pro programátory je neprogramovat mechanicky, tupě, metodou pokus-omyl. Bez koncepčního přístupu nás nespasí nic.
Miguel Primo,2008-07-24 14:28:09
Tomas Skopal: no hlavne cely tohle tema je skutecne o chybovosti konkretniho algoritmu, objektu, unity etc. To, na co vetsinou user poukazuje na chybu, je obvykle bud chyba funkcni implementace PL, nebo ergonomicka chyba - a to uz jde spis na konto pozadavku na kvalitu. Neco takovyho nezachrani - presne jak rikas - nic jinyho nez koncepcni prace.
Hezké :)
Michal Hanko,2008-07-24 12:12:47
To jsi hezky napsal "Programování je interaktivní proces mezi programátorem a spouštěním kódu."
Máš samozřejmě pravdu, tohle bych podepsal! :)
Zavádějící článek
Tomáš Skopal,2008-07-24 11:40:48
Nevím, nakolik se obsah tohoto článku shoduje s ideou těch vědců, ale
1) obecný program napsaný v bezkontextové gramatice je nerozhodnutelný, tj. nelze obecně ověřit, jestli vůbec skončí, natož jestli provede to co má....
2) tzn. formální verifikace (model checking, o kterém píšete) se musí uplatňovat na velmi úzké třídy programů
3) i tak je to velmi pomalé (exp.složitost), resp. nelze použít na rozsáhlé SW, na kterých by to zrovna bylo užitečné
4) verifikace probíhá tak, že se na programu se ověřuje platnost invariantů a jiných podmínek - ty se musí nějak zadefinovat pro každý program zvlášť, tj. programujete zase jiný program, kdo zkontroluje ten?
5) Tvrdit, že dnes se programuje špatně tím, že se narychlo napíše program a pak se opravuje je pomýlený názor... Srovnání s projektováním mostu je nemístné, protože most je jednoduchá šablona, mnohokrát použitá, i když se různé mosty liší, tak je to zejména v detailech, ne v principu. U SW je to úplně jinak. Navíc most se taky konstruuje iterativním způsobem, nikdy ne načisto. Nejprve architekt navrhne most, inženýži zrevidují statiku apod, tj. změní ho, ale tak aby to "nebylo vidět". V neposlední řadě při samotné stavbě mostu se zase dělají úpravy technického rázu (někde nepasují nějaké detaily). Je to prostě zcela přirozené, že se věci iterativně zlepšují... Konstrukce SW je navíc všechno v jednom architekt/programátor/optimalizátor/tester, program se nedá načisto napsat, sám slouží jako mezivýsledek, který se průběžně testuje. Proto je taky nesmysl učit studenty IT "programovat na tabuli", tj. načisto psát nějaký program. Programování je interaktivní proces mezi programátorem a spouštěním kódu.
Tj. závěrem - ten EU projekt se může zaměřovat na dílčí techniky/programy/jazyky, ale jestli vyvolává v laicích představu, že jsme jednou provždy zatočili s chybami v SW (jak zní nadpis tohoto článku), je to špatně. Nikdy to tak nemůže být...
Nesmysl
Michal Hanko,2008-07-24 10:20:51
Podle mě je to nesmysl. Důvod: Neexistuje algoritmus X, který by dostal na vstupu jiný algoritmus A, a rozhodl by v konečném čase, zda se X zacyklí nebo nezacyklí.
Zacyklení se je chyba programu. Proto jakýkoliv kontrolní program nemůže obecně rozhodnout o jakékoliv funkci, kterou dostane na vstupu, zda je napsána správně nebo ne. A proto to podle mě celé stojí na vodě...
Testovat, testovat, testovat
Miguel Primo,2008-07-24 01:41:27
Ja sice rozumim vsem tem software assurance procesum, a ze letecky navigacni sw proste takovym procesem projit musi, ale obecne mi neni tak docela jasne, na jake tema presne badatele badaji, kdyz badaji o bezporuchovosti software.
- Programator, ktery dusledne testuje, ma proste mensi
chybovost. A tim myslim vnitrni testy objektu,
ktere pise, testovat produkt musi naopak kdokoli jiny
krome autora (nebo testovaci procesor)
- Minimalne 35% chyb produktu je vec zadani a vetsinou
taky zadavatele (tj nejenze zadani je spatne, ale
ze zadavatel vlastne nevi, co chce a zjisti to az
kdyz dostane neco, co nechce)
- Nemalo selhani SW ma na svedomi okolni prostredi,
tedy predem nepredvidatelne interakce programu
a hostitelskeho prostredi nebo jinych programu
- Nic jineho na celem sirem svete nenajde ergonomicke
chyby, nez lidske oko. A jestli laik mluvi o chybe
programu, ma na mysli PREDEVSIM ergonomicke chyby
(krome fatalnich funkcnich samozrejme)
Z techto duvodu povazuji badani v tomto smeru za ponekud nehospodarne vynalozeny cas. Ano, pro matematika muze byt zajimave akademicky resit, jak by minimalizoval (nikoli eliminoval - nechtejte me rozesmat) chybovost vyvoje sw, ale doufam ze proboha neceka, ze se po vysledcich jeho prace vsichni nadsene vrhnou.
Pana Berana si vazim, ale tenhle clanek je IMHO - klidne me kamenujte - plny velmi neopatrnych tvrzeni. Nordström je mozna schopny matematik, ale jestli tvrdi, ze pomoci Types a podobnych akademickych experimentu zajisti bezchybovy vyvoj sw, mohl by mozna svuj talent zkusit zamerit na neco uzitecnejsiho.
nesrovnalosti
Peca Pospec,2008-07-23 19:18:01
Trochu mě zarazil překlad věty "Princip otevřeného zdroje je nezbytný...", autor pravděpodobně myslel pojem OpenSource, který se do češtiny většinou nepřekládá, nebo se překládá jako otevřený zdrojový kód programu (z kontextu to tak dle mého názoru nevyznělo).
Pokud stojí za to zmínit některé podpůrce formální analýzy programů, pak je to určitě Microsoft, který ročně investuje stovky milionů USD do software na automatickou verifikaci algoritmů, pozadu však nezůstávají ani výrobci hardware, například se Intel po své nechvalně známé chybě s dělením u Pentia snaží o formální verifikaci hardware. Bohužel tato tématika se rozvíjí velmi pomalu, protože stroje obecně nejsou schopny pochopit samy sebe. Například neexistuje algoritmus, který by o jakémkoliv jiném algoritmu s jistotou řekl, zda skončí v konečném čase.
U verifikací je také obrovský problém s explozí statového prostoru, takže efektivně automatizovaně se dají verifikovat jenom velmi krátké úseky kódu, operační systémy se zdrojovými kódy řádově o milionech řádků jsou prostě někde jinde.
Formální analýza software tu už dlouho je, problém je v tom, že není automatická a musí ji dělat člověk. Například software do raketoplánů se verifikuje, cena je ale řádově 1000x vyšší, než u běžného software.
Diskuze je otevřená pouze 7dní od zvěřejnění příspěvku nebo na povolení redakce