Программаның дұрыстығын дәлелдеу әдістері

  • <айнымалы> ← <өрнек>түрінде берілген меншіктеу операторын қарастырайық, мұнда “←” –меншіктеу амалының белгісі болады, ол әр программалау тілінде әр түрлі белгімен берілуі мүмкін, мысалы, “:=” –Pascal тілінде, “=”- Basic тілінде. Мнешіктеу операторының орындалуы екі этапта өтеді: алдымен өрнектің мәні есептелінеді, сонда кейін осы есептелінген мән айнымалыға меншіктеледі. Осылай, меншіктеу операторы айнымалы мәнін анықтау немесе қайта анықтау қызметін атқарады. Өрнектің мәнін есептегенде оған қатысатын айнымалының соңғы меншіктелінген мәні алынады;
  • Тізбектеу операторы күрделі S әрекеті өзінің құрамына кіретін және орындалулары бірінен кейін бірі болатын саны шекті S1,S2,…,SN операторларының тізімі анықтайды.
  • Тармақталу операторы үш түрге бөлінеді:

— қарапайым тармақталу күрделі S әрекеті белгілі В шартына байланысты берілген S1 әрекетін орындау керек немесе еш нәрсе орындамау керек дегенді көрсетеді;

-балама тармақталу күрделі S әрекет белгілі бір В шартына байланысты берілген S1 әрекетін немесе S2 әрекетін орындау керек дегенді көрсетеді;

-көп мәнді тармақталу кұрделі S әрекеті белгілі айнымалы шама V өзінің әр түрлі мүмкін 1,2,…, N мәндерінің біреуін міндетті түрде қабылдауына сәйкес берілген әр түрлі S1,S2,…,SN әрекетінің біреуі міндетті түрде орындалуы қажет дегенді көрсетеді.