The standard approach to automated Hoare-style program verification is to combine a weakest precondition calculus with a first order logic theorem prover. The calculus either needs explicit loop invariant annotations, or else an additional facility for loop invariant generation.
The alternative scheme we present in this thesis is to use a weakest precondition calculus which produces assertions in a richer language, which does not require loop invariant annotation or generation, but instead a more powerful theorem prover.
The main task of the thesis has been to investigate this approach and to evaluate its effectiveness on concrete examples. Experience from the prototype tool developed show that the approach has a few advantages but requires more research before it can solve any real interesting problems.
Den vanliga ansatsen till automatiserad, Hoare-baserad, programverifiering är att kombinera en kalkyl för svagaste förvillkor med en teorembevisare för första ordningens logik. Kalkylen behöver antingen explicita annoteringar för loop-invarianter eller någon facilitet för att generera sådana.
Den alternativa ansatsen vi presenterar här använder en kalkyl för svagaste förvillkor som producerar försäkringar i en rikare logik, vilken inte behöver någon annotering eller generering av loop-invarianter, men istället en mer kraftfull teorembevisare.
Huvuduppgiften i denna uppsats har varit att utforska denna ansats och evaluera dess effektivitet på konkreta exempel. Erfarenhet från prototypverktyget visar att ansatsen har några fördelar med behöver mer utforskning för att kunna lösa några riktigt intressanta problem.