A programkódban állításokat lehet elhelyezni, erre szolgál az assert utasítás. Ennek egy Boolean értékű kifejezést kell tartalmaznia, melyről feltételezzük, hogy a program azon pontján igaz értéket ad. Ha a tartalmazó blokk elején nem helyeztük el a checked kulcsszót, akkor a fordító ezt kommentnek tekinti; különben pedig futás közben kiértékeli a kifejezést, és ha False, a program abortál.
Pl.:
assert x<y and y<z
Az eljárásokhoz, függvényekhez elő- és utófeltételt lehet megadni (pre, post), melyek futás közben szintén ellenőrzésre kerülnek. A modulokhoz invariáns állítást (invariant) lehet megadni, melyről feltételezzük, hogy a modul változó élettartama alatt végig igaz (kivéve esetleg a modul eljárásainak futása közben). A fentiek csak checked tartalmazó blokkban értékelődnek ki futásidőben. A modulokhoz lehet absztrakciós függvényt is megadni, mely a modul helyesség-bizonyításához szükséges. Ez a függvény a modulon belüli változókat képezi a modul típus egy értékére.
Fordító által generált állítások: abban az esetben, ha a fordítónak muszáj bizonyos feltételeket igaznak tekinteni, de képtelen kikövetkeztetni, hogy azok igazak-e, generálhat állításokat (egy programlistában) a bizonyító számára, és utána azokat biztosnak tekintheti. A program érvényessége ezek után a fordító által generált állítások igazságától függ.
A következő példa a modul típusnál bemutatott verem modul ellenőrzött változata:
type Stack (Stacksize: unsignedInt) = module
exports (Pop, Push)
checked
var IntStack: array 1..StackSize of signedInt
var StackPtr: 0..StackSize := 0
procedure Push (X: signed Int) =
imports (var IntStack, StackPtr, StackSize)
pre StackPtr in 0 .. StackSize-1
post IntStack(StackPtr) = X
begin
StackPtr := StackPtr+1;
IntStack(StackPtr) := X;
end Push
procedure Pop (var X: signedInt) =
imports (var IntStack, StackPtr)
pre StackPtr in 1 .. StackSize
post X = IntStack (StackPtr-1)
begin
X := IntStack(StackPtr);
assert X=IntStack(StackPtr);
StackPtr := StackPtr-1;
end Pop
invariant StackPtr in 0 .. StackSize
end Stack