Sciencemag.cz
Doporučujeme
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?
