Propos liminaire (Introduction à la vérification de programme) (Version intégrée)