Worldlex Wiki Une transformation de programme est une opération qui prend un programme informatique et génère un autre programme. Dans de nombreux cas, le programme transformé doit être sémantiquement équivalent à l'original, par rapport à une sémantique formelle particulière et dans moins de cas, les transformations aboutissent à des programmes qui diffèrent sémantiquement de l'original de manière prévisible.
Bien que les transformations puissent être effectuées manuellement, il est souvent plus pratique d'utiliser un système de transformation de programme qui applique les spécifications des transformations requises. Les transformations de programme peuvent être spécifiées sous forme de procédures automatisées qui modifient les structures de données du compilateur (par exemple, des arbres de syntaxe abstraits ) représentant le texte du programme, ou peuvent être spécifiées de manière plus pratique à l'aide de modèles ou de modèles représentant des fragments de code source paramétrés.
Une exigence pratique pour les systèmes de transformation de code source est qu'ils soient capables de traiter efficacement les programmes écrits dans un langage de programmation . Cela nécessite généralement l'intégration d'un frontal complet pour le langage de programmation concerné, y compris l'analyse du code source , la création de représentations internes des structures de code, la signification des symboles du programme, des analyses statiques utiles et la régénération du code source valide à partir des représentations du programme transformées. Le problème de la création et de l'intégration de frontaux adéquats pour les langages conventionnels ( Java , C++ , PHP , etc.) peut être aussi difficile que la création du système de transformation de programme lui-même en raison de la complexité de ces langages. Pour être largement utile, un système de transformation doit être capable de gérer de nombreux langages de programmation cibles et doit fournir des moyens de spécifier ces frontaux.
Une généralisation de l'équivalence sémantique est la notion de raffinement de programme : un programme est un raffinement d'un autre s'il se termine sur tous les états initiaux pour lesquels le programme original se termine, et pour chaque état de ce type, il est garanti de se terminer dans un état final possible pour le programme original. En d'autres termes, un raffinement d'un programme est plus défini et plus déterministe que le programme original. Si deux programmes sont des raffinements l'un de l'autre, alors les programmes sont équivalents.