Ohjelmisto
Mikä on haamu koodauksessa?
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.