JavaScript: de la standardisation à la formalisation
Résumé
JavaScript est un langage complexe, mais dont la sémantique est très
précisément définie.
Il est donc envisageable de formellement prouver la
correction d'un programme JavaScript étant donnée une formalisation de sa
sémantique. Dans cet exposé, nous décrirons rapidement le langage, en
insistant sur les aspects les plus surprenants.
Nous motiverons le besoin d'une formalisation du langage dans un assistant de preuve et montrerons
quelles formes elle peut prendre. Nous décrirons enfin les retombées de cette
formalisation vis à vis du processus de standardisation, ainsi que ses
différentes utilisations.
