Deduktiivisen ohjelman todentamisen yhteydessä haamukoodi on osa ohjelmaa, joka lisätään määrittelyä varten. Haamukoodi ei saa häiritä tavallista koodia siinä mielessä, että se voidaan pyyhkiä ilman havaittavia eroja ohjelman tuloksessa.
Mikä on haamu koodauksessa?
