Quale rappresentazione formale è comunemente usata per descrivere le ottimizzazioni del compilatore?

Question

Ho ideato un'ottimizzazione del compilatore che funzioni su qualsiasi linguaggio strutturato che dispone di assegnazioni di array array[index] = value e conteggiti loop (for i = n; i < N; i++) {doTHIS} (*).

Ora voglio rappresentare questa ottimizzazione usando alcune semantiche formali. Dato che voglio pubblicare i miei risultati in un luogo di linguaggio di programmazione, vorrei sapere:

Quali sono le rappresentazioni formali (i) (sono) più comunemente usate per descrivere le ottimizzazioni del compilatore?

Ho già descritto la mia ottimizzazione usando la semantica operativa, ma attualmente sto esaminando questa scelta. Quindi, sono venuto alla comunità per un consiglio.

(*) Per favore perdona questa rappresentazione simile a C in una domanda che richiede semantica formale.