«İşləyir» görünən alqoritm hələ düzgün deyil. Düzgünlüyü əsaslandırmaq üçün ön şərt, son şərt və dövr invariantı anlayışlarından istifadə edirik.
Düzgün alqoritm nə deməkdir
Alqoritm düzgündür, əgər ön şərti ödəyən hər girişdə dayanır və son şərti ödəyən nəticə verir.
- Ön şərt (precondition) — girişin ödəməli olduğu şərt, məsələn, siyahı boş deyil.
- Son şərt (postcondition) — nəticənin ödəməli olduğu şərt, məsələn,
bestsiyahının ən böyük elementidir.
Ön şərt pozulubsa, alqoritm heç nə vəd etmir: səhv çağıran tərəfdədir.
Dövr invariantı
İnvariant dövrün hər təkrarından əvvəl doğru olan iddiadır. Onun üç mərhələsini yoxlayırıq:
- Başlanğıc — dövrdən əvvəl invariant doğrudur.
- Saxlanma — təkrarın əvvəlində doğrudursa, sonunda da doğrudur.
- Sonlanma — dövr bitəndə invariant və çıxış şərti son şərti verir.
