Hlavní navigace

Názor k článku Programovací jazyk Ada pro úplné začátečníky od Radek Miček - K veci - jak muze takova chyba vubec...

  • Článek je starý, nové názory již nelze přidávat.
  • 2. 5. 2015 11:16

    Radek Miček (neregistrovaný) ---.net.upcbroadband.cz

    K veci - jak muze takova chyba vubec vzniknout? Nepouzivaji se formalni metody jako napr. abstraktni interpretace?

    Formálně ověřit nějakou vlastnost může být docela náročné. Pokud tedy nástroj pro analýzu programu řekne, že něco neumí ověřit, tak se to IMO většinou nechá na lidech.

    Navíc může být chyba v HW, chyba v kompilátoru jazyka, chyba v nástroji, co ověřuje vlastnosti programů - málokdy má kompilátor nebo pomocný SW formální důkaz správnosti.

    Vše je navíc komplikováno faktem, že jazyky nemají formální specifikace.