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?

autor Continentaleurope, zdroj: Wikipedia, licence obrázku GFDL

Bonobové pomáhají cizincům i bez požádání

Člověk (mnohdy) podrží dveře někomu, kdo jde za ním. Nebo podepře někoho, kdo klopýtne. A …

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