Program Equivalence by Circular Reasoning
Résumé
We propose a deductive system for automatically proving the equivalence of programs written in deterministic languages that have a formal, term-rewriting based operational semantics. Symbolic programs (i.e., programs in which some statements or expressions are symbolic variables) can also be proved equivalent using the proposed approach. The deductive system is circular in nature and is proved sound and weakly complete; together, these results say that, when it terminates, our system correctly solves the program-equivalence problem as we state it. We show that the deductive system is suitable for proving equivalence both for terminating and non-terminating programs. We also report on a prototype implementation of the proposed system in the $\mathbb{K}$ framework
Nous proposons un systéme déductif pour prouver l'équivalence de programmes dans des langages déterministes munis de sémantiques opérationnelles définies par réécriture. Les programmes dits symboliques, dans lesquels certaines expressions ou instructions restent non-interprétés, peuvent également être traités par notre approche. Le systéme déductif proposé est circulaire; nous démontrons qu'il est correct et faiblement complet. Ces deux résultats signifient que notre systéme résout correctement le probléme d'équivalence de programmes tels que nous l'avons posé. Nous montrons que ce systéme fonctionne autant pour des programmes qui terminent que pour des programmes qui ne terminent pas. Enfin, nous décrivons une implémentation prototype de notre systéme déductif dans la \emph{$\mathbb{K}$ framework}.
Domaines
Systèmes embarqués
Origine : Fichiers produits par l'(les) auteur(s)