A NICE nyelv 2 fő helyességbiztosító nyelvi elemmel rendelkezik. Az első az un. assertion-ök használata, amelyek segítségével a program különböző pontjain őrfeltételeket helyezhetünk el, ezzel biztosítva, hogy a program további részén teljesülnek az invariánsok, illetve az előfeltételek. Ezek használata szintaktikailag megegyezik a JAVA hasonló nyelvi elemével:
// példa a ho, mint 1..12 egész szám típusinvariánsának ellenőrzésére
void setHonap( int ho ){
(ho > 0 && ho < 12) : “Csak 1 és 12 közötti szám adható meg paraméterként!”;
}
A másik lehetőség a szerződések (contracts) használata, amelyekkel az egyes metódusokhoz elő- és utófeltételeket rendelhetünk. Az elő- és utófeltételek assertion-ök alakjában adhatóak meg a függvénytörzs előtt a requires és ensures kulcsszavak segítségével. A fordítóprogram (amennyiben ezt engedélyezzük) automatikusan ellenőrizni fogja ezen feltételek teljesülését. Az előfeltételek ellenőrzésére a metódus törzs futtatása előtt kerül sor, az utófeltételeket pedig a törzs utolsó utasításának végrehajtása után ellenőrzi a program. A requires kulcsszó az előfeltételeket vezeti fel, az ensures kulcsszó pedig az utófeltételeket.
// Az alábbi példában egy puffersablon hozzáadás műveletének
// deklarációját láthatjuk, amely elő és utófeltételeket
// is állít fel, amelyeket a később az interfészt megvalósító
// osztály isEmpty és add metódusának teljesíteni kell
interface Buffer
{
int size();
boolean isFull();
boolean isEmpty() ensures result == (size() == 0);
void add(Elem element)
requires
!isfull() : "buffer must not be not full"
ensures
!isEmpty() : "buffer must not be empty",
size() == old(size()) + 1 : "count inc";
}