Fluctuat - Fluctuat

tento článek může být pro většinu čtenářů příliš technická na to, aby je pochopili. Prosím pomozte to vylepšit na aby to bylo srozumitelné pro neodborníky, aniž by byly odstraněny technické podrobnosti. (Leden 2013) (Zjistěte, jak a kdy odstranit tuto zprávu šablony)

Fluctuat byl vyvinut společností Alternativy komisariátu à l'Énergie Atomique et aux Énergies od roku 2001. Fluctuat umožňuje statickou analýzu C a Ada programy se zvláštním zaměřením na operace s plovoucí desetinnou čárkou.

Teoretické základy

Fluctuat je statický analyzátor, založený na abstraktní interpretace. Ve srovnání s podobnými nástroji jako Polyprostor nebo Astrée, spoléhá se na to zonotopy jako abstraktní doména. To znamená, že hodnota každé programové proměnné je abstrahována lineárním výrazem symboly hluku (interní proměnné, které se pohybují v [-1,1]).

Zvažme nyní následující program:

x = [0,1]; y = 2 * x + 1; z = x * y;

První řádek znamená, že hodnota X může být cokoli v [0,1]. Může být napsán jako x = 0,5 + 0,5 * ε, kde ε je symbol šumu. Druhý řádek to naznačuje y = 2 + ε; od té doby X a y sdílejí stejný symbol šumu, tato abstraktní doména je relační. Pokud existují nelineární operace, jako ve třetím řádku, jsou zavedeny nové symboly šumu. Přesný symbolický výraz by byl z = 1 + 1,5 * ε + 0,5 * ε * ε, ale abstrahujeme to jako z = 1,25 + 1,5ε + 0,25η.

Funkce

Mezi funkce Fluctuat patří:

• statická analýza z C a Ada programy.^[1]
• Analýza citlivosti programových proměnných.^[2]
• nejhorší případ generace.
• interaktivní analýza.
• analýza hybridní systémy ^[3]

Viz také

• Statická analýza kódu
• Abstraktní interpretace
• Seznam nástrojů pro statickou analýzu kódu

Reference

externí odkazy

• Oficiální webové stránky