Inden for mange områder er det essentielt at softwaren er korrekt. Inden for datalogien er der udviklet en række formelle verifikation teknikker, herunder statisk analyse og model tjek, som gør det muligt at analysere softwaren og sikre at den har forskellige egenskaber. I denne afhandling præsenteres en ramme inden for hvilken man hurtigt og elegant kan specificere specielt statisk analyse og model tjek problemer i logisk form. Denne ramme understøttes af en række generiske værktøjer, som gr at man givet en egenskab automatisk kan konstruere et system som kan analysere softwaren for den pågældende egenskab.I den første del af afhandlingen præsenteres en gitter-baseret logik kaldet Least Fixed Point Logic (LLFP). Dens semantiske fundament er en matematiske struktur af fuldstændige gitre som tilfredsstiller den såkaldte Ascending chain condition. Vi viser at LLFP har en Moore familie egenskab; det betyder at ethvert problem udtrykt i LLFP altid har præcist en løsning som er bedre en alle andre løsninger på problemet. Vi udvikler derefter en implementation som beregner denne løsning; den er baseret pa den såkaldte differential worklist tilgangsvinkel.Den næste logik der præsenteres i afhandlingen er Layered Fixed Point Logic. Denne logik adskiller sig fra den forrige ved at den direkte understøtter induktive såvel som co-induktive specifikationer af problemer. Også for denne logik viser vi en Moore familie egenskab; ydermere etablerer vi et worst-case tids kompleksitets resultat. Denne gang udvikler vi en implementation baseret påBDD tilgangsvinklen; implementationen beregner den bedste løsning på problemet, som angivet af Moore familie resultatet, og har en køretid svarende tildet teoretiske kompleksitets resultat.Efterfølgende studerer vi en optimeringsstrategi, kaldet magic sets transformationer, fra deduktive databaser og dens anvendelse pa logikken ALFP. Ideen er at omskrive den oprindelige formulering af egenskaben til en form som muliggør en mere effektiv beregning; specielt er det ikke nødvendigt at beregne hele løsningen hvis der kun er brug for en mindre del af den.I den sidste den af afhandlingen illustrerer vi hvordan logikkerne og de tilhørendeimplementationer kan bruges til hurtig konstruktion af prototyper. Specielt servi pa forskellige eksempler fra statisk analyse og model tjek.
展开▼
