شرطی که قبل و بعد از هر دور حلقه درست است. آن را مینویسید، نشان میدهید در شروع برقرار است، هر قدم آن را حفظ میکند و وقتی حلقه تمام شد نتیجه از آن درمیآید.
Invariant
شرطی که قبل و بعد از هر دور حلقه برقرار است و برای اثبات درستی الگوریتم به کار میرود.