1. Introduction
Afin de rendre les programmes plus sûrs, une approche mathématique de la programmation fut recherchée depuis les années 50. Celles-ci nous amènent à la preuve de programme, qui se caractérise comme étant la démonstration que les spécifications formelles d'un programme sont vraies. La spécification consiste à décrire très précisément ce que fait le programme. Si le programme est conforme à ses spécifications, le programme est considéré comme sûr [7][8].
À quel point un programme prouvé mathématiquement est sûr ? Et comment être sûr du vérificateur de preuve, sed quis custodiet ipsos custodes ? La sûreté du programme dépend des spécifications formulées. En effet, plusieurs classes de spécifications doivent être décrites afin d'obtenir une grande sûreté du programme. De plus, les vérificateurs de preuves font aujourd'hui encore l'objet de recherches poussées, un domaine en pleine ébullition, et de contrôles assidus (par exemple...
- Accédez à tous les contenus de Connect en illimité
- Découvrez des listes de lecture et des contenus Premium
- Consultez les nouveaux articles en avant-première