Foto: kentoh / Dollar Photo Club

Programy s matematicky ověřovanou funkčností

V rámci Defense Advanced Research Projects Agency (DARPA) a řady dalších institucí (Tufts University, Princeton University a Microsoft Research) probíhají pokusy o tvorbu kódu, jehož spolehlivost by byla ověřena formálně – tedy podobně jako matematický důkaz. U kódů tohoto typu by mělo být ověřeno, že bez ohledu na podobu vstupu (nelze testovat veškeré možné hodnoty) nebudou provádět žádnou nepředpokládanou aktivitu – podobně jako u matematického důkazu není např. třeba testovat, že určitá rovnice platí pro veškerá možná x. Projekty „verifikovaného kódu“ mají historii táhnoucí se až do 70 let. Jak upozornil Quanta Magazine, nyní se tímto způsobem ale zkoušejí vytvářet i kódy pro kritické systémy či zařízení (vojenské drony, satelity, automobily apod.), v Microsoft Research se takto testuje i možný nástupce protokolu http jménem Everest.

Zdroj: Quanta Magazine

Poznámky:
Budou existovat nerozhodnutelné případy, zda algoritmus opravdu dělá něco? (Viz problém zastavení, nemožnost obecně rozhodnout, zda algoritmus X řeší problém Y nejrychleji.) To ale neznamená, že fungování případu nepůjde určit pro „normální“ případy. Má nerozhodnutelnost nějaký praktický význam z hlediska bezpečnosti?
Je-li program napsán ve vyšším programovacím jazyce a běží-li na operačním systému – lze vůbec něco garantovat, když do hry vstupuje kompilátor/interpretr a samotný operační systém?

nástroj z paleolitu, credit (c) University of Tübingen

Neu5Gc: pomůže mutace rekonstruovat evoluci člověka?

Dochovaná fosilní DNA stará miliony let je dosud pouze zbožným přáním, nicméně evoluci člověka by …

Používáme soubory cookies pro přizpůsobení obsahu webu a sledování návštěvnosti. Data o používání webu sdílíme s našimi partnery pro cílení reklamy a analýzu návštěvnosti. Více informací

The cookie settings on this website are set to "allow cookies" to give you the best browsing experience possible. If you continue to use this website without changing your cookie settings or you click "Accept" below then you are consenting to this.

Close