Изҳороти пурраи дурустӣ низ қисман изҳороти дуруст аст. Дурустии қисман заифтар аст, зеро барои расидан ба хулоса ба кӯмаки иловагии 'S terminates' ниёз дорад: R дар ҳолати ниҳоӣ татбиқ мешавад.

Барои мушаххасоти дурустии қисман дурусти {Q} S {R} шумо метавонед маълумоти зеринро гиред: Агар шарти ибтидоӣ вуҷуд дошта бошад, ки Q, S метавонад ба итмом расад ё тамом нашавад. Агар S хотима ёбад, пас аз иҷрокунии S, шумо ба ҳолати ниҳоӣ мерасад, ки R-ро иҷро мекунад. Дар акси ҳол, Р корношоям аст, зеро ягон ҳолати ниҳоӣ мавҷуд нест.

Масалан:

{x == 10} дар давоми (y! = 0): y = y - 1 x = 0 {x == 0}

Ин як изҳороти саҳеҳии дақиқ аст. Агар y бо рақами баробар ба 0 ё калонтар оғоз карда шавад, S хотима меёбад ва он гоҳ х 0 мешавад. Агар y аз рақами манфӣ оғоз шавад, S абад такрор мешавад ва азбаски он ба охир нарасидааст, шумо ба ҳолате намерасед. 'баъд аз қатли С.'

Дар асл, R метавонад чизе бошад, агар S ҳалқаи мурда бошад. Масалан барои ҳар як савол ва R:

{Q} дар давоми (ҳақиқӣ): y = y - 1 {R}

ҳамеша нишондиҳандаи қисман дуруст аст.

Агар Q кофӣ набошад, шумо наметавонед ба анҷом расидани S-ро кафолат диҳед, танҳо пас аз иҷрои С. Дар ин ҳолат шумо метавонед як шартро ба таври дастӣ илова кунед: S abort. Далелро метавон бо Q ва он идома дод.

Барои тавсифи пурраи дурустии {Q} S {R}, Q қавӣ аст, ки қатъшавии S-ро кафолат медиҳад, то шумо хулоса бароред, ки S қатъ карда мешавад ва ҳолати ниҳоии R қонеъ карда мешавад.

Масалан:

{x == 10} дар давоми (x! = 0): x = x - 1 {x == 0}

як изҳороти дақиқ комил аст.

Бо роҳи: Ман боварӣ надорам, ки ҷавоб дуруст аст, зеро савол бо дурустии сиёсӣ ишора шудааст. Дар ҳоле, ки таъриф дар савол ба мисли илми информатика якхела аст.