afm09-why-tutorial

Description

Why—an intermediate languagefor deductive program verificationJean-Christophe FilliˆatreCNRSOrsay, FranceAFM workshopGrenoble, June 27, 2009Jean-Christophe Filliˆatre Why tutorial AFM’09 1 / 56Motivationshow to do deductive program verification on realistic programs?deductive verification means that we want to prove safety but alsobehavioral correctness, with arbitrary proof complexityrealistic programs means pointers, aliases, dynamic allocation,arbitrary data structures, etc.Jean-Christophe Filliˆatre Why tutorial AFM’09 2 / 56Motivationssince Hoare logic (1968), we know how to turn a program correctnessinto logical formulas, the so-called verification conditionswe coulddesign Hoare logic rules for a real programming languagechoose an interactive theorem proverthe Why approach: don’t do that!Jean-Christophe Filliˆatre Why tutorial AFM’09 3 / 56Principlesinstead,design a small language dedicated to program verificationand compile complex programs into ituse as many theorem provers as possible (interactive or automatic)Jean-Christophe Filliˆatre Why tutorial AFM’09 4 / 56Related Workthere is another such tool: the Boogie tool developed at MicrosoftResearch, initially in the context of the SPEC# project (Barnett, Leino,Schulte)there are differences but the main idea is the same: verification conditionsshould be computed on a small, dedicated languageJean-Christophe Filliˆatre Why tutorial AFM’09 5 / 56Overview1 theWhy languageand its ...

Informations

• Publié par: Endrui
• Nombre de lectures: 12
• Langue: English

Extrait

Jean-ChritspoehFilliˆarte

Why — an intermediate language for deductive program verification

Jean-ChristopheFilliˆatre

CNRS Orsay, France

AFM workshop Grenoble, June 27, 2009

WhytutorialFA’M901/56

Motivations

J

how to dodeductive program verificationon realistic programs?

ae-nhCri

deductive verification means that we want to prove safety but also behavioral correctness, with arbitrary proof complexity

realistic programs means pointers, aliases, dynamic allocation, arbitrary data structures, etc.

stopheiFllaˆirteWhytutorialAFM’092/56

Motivations

J

sinceHoare logic(1968), we know how to turn a program correctness into logical formulas, the so-called verification conditions

we could design Hoare logic rules for a real programming language choose an interactive theorem prover

the Why approach:don’t do that!

ae-nhCirtsopheFilliˆarteWhytturoialAFM’093/56

Principles

J

instead,

ean-Chri

design asmalllanguage dedicated to program verification and compile complex programs into it

use asmany theorem proversas possible (interactive or automatic)

tspoehiFllˆiatreWhytutorialFAM’094/56

Related Work

J

there is another such tool: theBoogietool developed at Microsoft Research, initially in the context of the SPEC# project (Barnett, Leino, Schulte)

there are differences but the main idea is the same: verification conditions should be computed on a small, dedicated language

ae-nhCirtspoehiFllaiˆtreWhytutorialFAM’095/56

complete example with a C program

2

Whyas an intermediate language for program verification

6/5

1

and its application to the verification of algorithms

Overview

theWhylanguage

iˆatreWhopheFillAlMF0’69tyturoaitsirhC-naeJ

The essence of Hoare logic

J

the essence of Hoare logic fits in the rule for assignment

{P[x←E]}x:=E{P}

two key ideas there isno alias, since only variablexis substituted thepureexpressionEbelongs to bothlogic and program

ae-nhCritspoehFillˆaitreWhytutorialFA’M907/56

iˆllreatopstFihe-naeirhCJ

the sole data structures are mutable variables containing pure values

programs can manipulate pure values (i.e. logical terms) arbitrarily

any program that would create an alias is rejected

6

The essence of Hoare logic

Whycaptures these ideas

98/5MF0’aiAlturohWty

Structure of aWhyFile

aWhyfile contains

logical declarations logica:int logicf:int, int -> int axiomA:forall x:int. ... typeset

program implementations letp2 (x:int) (y:int) = ...

/56

variable/program declarations parameterx:intref parameterp1:a:int -> ...

striChn-eaJerhWˆitaiFllpoeh’099lAFMoriaytut

Predefined Types

J

a few types and symbols are predefined a typeintof arbitrary precision integers, with usual infix syntax a typerealof real numbers a typeboolof booleans a singleton typeunit

ean-ChristopheFilliˆatrehWyttuorilaFA’M9010/56

6

one nice idea taken from functional programming: no distinction between expressions and statements

ML Syntax

butWhyis not at all a functional language

⇒less constructs, thus less rules ⇒side-effects in expressions for free

othprhsinaC-eJ5/1190’MFAlairottuhyeWtrˆaliileF