Cet article traite de propriétés formelles des langages de programmation dont le but est de vérifier, voire prouver, que les programmes fonctionnent correctement. Dans un contexte de processus centré sur les modèles (processus IDM), ces propriétés peuvent être appliquées à des langages de modélisation pour garantir la qualité attendue de la part des modèles, et la cohérence entre les modèles et les programmes. Mais ces techniques de preuve, basées sur la logique des prédicats, peuvent-elles s'appliquer à des langages métiers tels que le langage «Structured Analysis Model» (SAM) développé pour modéliser des applications du domaine de l'aéronautique ?