Кіріспе

Инвариантқа негізделген бағдарламалау – нақты бағдарламалық операторлардан бұрын спецификациялар мен инварианттар жазылатын бағдарламалау әдістемесі. Бағдарламалау процесінде инварианттарды жазудың бірнеше артықшылықтары бар: ол бағдарламашыдан бағдарламаның мінез-құлқы туралы ниеттерін нақты іске асырудан бұрын анықтауды талап етеді, ал инварианттарды орындау кезінде динамикалық түрде бағалауға болады, осы арқылы жиі кездесетін бағдарламалау қателіктерін анықтауға мүмкіндік туады. Сонымен қатар, егер инварианттар жеткілікті күшті болса, бағдарламалық операторлардың формальды семантикасына негізделген бағдарламаның дұрыстығын дәлелдеу үшін оларды пайдалануға болады. Тривиальды емес бағдарламаларды толық тексеру үшін, әдетте, қуатты формальды дәлелдеу жүйесімен байланыстырылған біріктірілген бағдарламалау және спецификация тілі қажет болады. Мұндай жағдайда дәлелдеуді автоматтандырудың жоғары деңгейіне де қол жеткізуге болады. Қазіргі қолданыстағы бағдарламалау тілдерінің көпшілігінде негізгі ұйымдастыру құрылымдары – бақылау ағыны блоктары, мысалы, for циклдары, while циклдары және if операторлары. Мұндай тілдер инварианттарды бірінші кезекте бағдарламалау үшін идеалды болмауы мүмкін, себебі олар бағдарламалаушыны инварианттарды жазудан бұрын бақылау ағыны туралы шешім қабылдауға мәжбүрлейді. Сонымен қатар, көптеген бағдарламалау тілдері спецификациялар мен инварианттарды жазу үшін жеткілікті қолдау көрсетпейді, өйткені оларда квантор операторлары жетіспейді және көбінесе жоғары реттік қасиеттерді білдіру мүмкін болмайды. Бағдарламаны оның дәлелдемесімен бірге әзірлеу идеясы Э. В. Дейкстраға тиесілі. Бағдарламалық операторлардан бұрын инварианттарды жазуды М. Х. ван Эмден, Дж. С. Рейнольдс және Р. Дж. Бэк түрлі формаларда қарастырған.