Langages de programmation et compilation

Jean-Christophe Filliâtre

Description

Ecole Normale Superieure
Langages de programmation
et compilation
Jean-Christophe Filli^atre
Cours 4 / 21 octobre 2010
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 1 / 77Typage
+
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 2 / 77Typage
/
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 3 / 77Typage
si j’ecris l’expression
"5" + 37
dois-je obtenir
une erreur ? (Caml)
l’entier 42 ? (Visual Basic)
la cha^ ne "537" ? (Java)
autre chose encore ?
et qu’en est-il de
37 / "5"
?
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 4 / 77Typage
et si on additionne deux expressions arbitraires
e1 + e2
comment determiner si cela est legal, et ce que l’on doit faire le cas
echeant ?
la reponse est le typage, une analyse statique du programme qui associe
un type a chaque sous-expression, dans le but de rejeter les programmes
incoherents mais aussi de permettre la compilation
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 5 / 77Slogan
well typed programs do not go wrong
Jean-Christophe Filli^atre Langages de programmation et compilation 2010{2011 / cours 4 6 / 77Objectifs du typage
le typage doit ^etre decidable
le typage doit rejeter les programmes absurdes comme 1 2, dont
l’evaluation echouerait ; c’est la suret^ e du typage
le typage ne doit pas rejeter trop de programmes ...

Sujets

• cours

Informations

• Publié par: Adri
• Nombre de lectures: 166
• Langue: Français

Extrait

-CanJehpotsirhaˆilliFeegdspeorrtLenaagonetcompgrammati–0101102tali2noi7/7

Cours 4 / 21 octobre 2010

Jean-ChristopheFilliˆatre

Langages de programmation et compilation

´ EcoleNormaleSup´erieure

ou/c41rs

Typage

Jean-Christophe

Filliˆatre

+

Langages

de

programmation

et

compilation

2010–2011

/

cours

4

2

/

77

Typage

Jean-Christophe

Filliˆatre

/

Langages

de

programmation

et

compilation

2010–2011

/

cours

4

3

/

77

mmaroitaedsegorptila20ontcnepiomirtspoehJae-nhCreLangagFilliˆat

?

37 / "5"

et qu en est-il de ’

dois-je obtenir une erreur ? (Caml) l’entier 42 ? (Visual Basic) lachaıˆne"537"? (Java) autre chose encore ?

Typage

77

"5" + 37

sij’´ecrisl’expression

1/01–2104/s4urco

irhC-naeJ/577ru4s

lar´eponseestletypage, une analyse statique du programme qui associe untypeesrammproguqseuo-s`caah,donslanprexsiesetejselrtubeered incoh´erentsmaisaussidepermettrelacompilation

commentde´terminersicelaestle´gal,etcequel’ondoitfairelecas e´cheant? ´

Typage

e1 + e2

et si on additionne deux expressions arbitraires

tspoehiFllˆitaerLangagesdeprogratammenoimoctaliponti102001–2co1/

oitalipmoctenoitmaamgrroepsdgega

wrong

go

programs

typed

not

do

7

well

Slogan

647/ours11/c0–20n201aˆrtLenahpFeliil-ChristoJean

le typage ne doit pas rejeter trop de programmes non-absurdes, i.e.syle`estiodsteˆtedemepyterexpressif

ipalitno02012–101/cours47/77

Objectifs du typage

letypagedoitˆetreadice´delb

le typage doit rejeter les programmes absurdes comme 1 2, dont l’´evaluation´echouerait;c’estlaeagyputedt´reˆus

gnaLertarpedsegaatmmraogomtcneioae-nJstopChrilliˆheFi

gagesdepˆatreLanhpFeliilC-rhsiot01n2200–ilmpioatnoitoctergoramma

annoterseulementlesparam`etresdefonctions

fun(x:int)→lety= +(x,1)iny

annoter seulement les variables (Pascal, C, Java, etc.)

2

fun(x:int)→let(y:int) = +(x,1)iny

3

ne rien annoter⇒nineec´free,lleksa).ctetl`mpco,HmlCae(

1

touteslessous-expressionssontannot´eesparuntype

faciledeve´rifiermaistropfastidieuxpourleprogrammeur

7

4

Plusieurs solutions

847/uosr11c/naeJ tni×tni)i:tn))i::int),(1(+:)(((xi:y(=)tn)tnitel→fux:n(n

aneLtrˆaliileFphotsirhC-naeJ

unalgorithmedetypagedoitavoirlesproprie´t´esde correctione´remhtirogla’lilerslo”aui“ondpoeetsarmmrpgo:s effectivementbientyp´e

compl´etudeemhtirogtiod,a´eypntall’rslorgmapeorbteiemse:sil repondre “oui” ´

/749

Propri´ete´sattendues

et´eventuellementde principalit´eeral´en´lusgltpenoseseisxerplace´lucuopeenur:lypet possible

7c/11sruo102n02–0mpilatiotionetcoorrgmaamagegdspe

seedgngaeraLˆitanetcatiorammprogaeJllFiheopstriChn-

id´rons le typage de mini-ML cons e

Typage de mini-ML

1 2

typage monomorphe typagepolymorphe,inf´erencedetypes

02no2–01ipmoital10s47/71/01urco

10–2on20cour011/encttaoialitmoip77/114s

identificateur constante (1, 2, . . .,true . .), . primitive (+,×,fst, . . .) fonction application paire liaison locale

x c op funx→e e e (e,e) letx=eine

::= | | | | | |

e

rappel

mini-ML

Jean-ChristagngdeesogprmmraehpolliFtaˆiaLer