Nel contesto della verifica deduttiva del programma, il codice fantasma fa parte del programma che viene aggiunto ai fini della specifica. Il codice Ghost non deve interferire con il codice normale, nel senso che può essere cancellato senza differenze osservabili nell’esito del programma.
