Кіріспе

Флойд-Хоар логикасының қайта формулировкасы. Предикатты трансформатор семантикасын Эдсгер Дайкстра өзінің "Қоршалған командалар, белгісіздік және бағдарламалардың формалды туындылануы" атты мақаласында енгізді. Олар императивті бағдарламалау парадигмасының семантикасын осы тілдегі әрбір операторға сәйкес келетін предикат трансформаторы арқылы анықтайды: оператордың күй кеңістігіндегі екі предикат арасындағы толық функция. Осы тұрғыдан алғанда, предикатты трансформатор семантикасы – денотациялық семантиканың бір түрі. Шындығында, қоршалған командаларда Дайкстра тек бір түрдегі предикат трансформаторын қолданады: жақсы белгілі ең әлсіз алғышарттар (төменде қараңыз). Сонымен қатар, предикатты трансформатор семантикасы – Флойд-Хоар логикасының қайта формулировкасы болып табылады. Хоар логикасы дедуктивті жүйе ретінде ұсынылса, предикатты трансформатор семантикасы (ең әлсіз алғышарттар немесе ең күшті постшарттар арқылы, төмендегідей) – Хоар логикасының дұрыс дедукцияларын құрудың толық стратегиялары болып табылады. Басқаша айтқанда, олар Хоар үштігін тексеру мәселесін бірінші реттік формуланы дәлелдеу мәселесіне дейін азайтуға мүмкіндік беретін тиімді алгоритмді ұсынады. Техникалық тұрғыдан алғанда, предикатты трансформатор семантикасы операторларды предикаттарға символдық түрде орындауды жүзеге асырады: орындалу ең әлсіз алғышарттар жағдайында кері бағытта, ал ең күшті постшарттар жағдайында тікелей бағытта жүреді.

Анықтама

S мәлімдемесі және R постшарты үшін ең әлсіз алғышарт – кез келген алғышарт P үшін, егер және тек егер орындалса, Q предикаты болып табылады. Басқаша айтқанда, бұл S орындалғаннан кейін R орындалуын қамтамасыз ету үшін қажетті "ең әлсіз" немесе ең аз шектеулі талап. Бірегейлік анықтамасынан оңай шығады: егер Q және Q' екеуі де ең әлсіз алғышарттар болса, онда анықтамасы бойынша және , демек . S мәлімдемесі үшін R постшартымен салыстырылған ең әлсіз алғышартты білдіру үшін біз жиі қолданамыз.

Конвенциялар

Біз T-ны әрқашан дұрыс болатын предикатты, ал F-ны әрқашан жалған болатын предикатты белгілеу үшін қолданамыз. Біз, кем дегенде, қандай да бір тілдің синтаксисімен анықталған және дұрыс және жалған бұлдік мәндерін қамтитын бұлдік өрнектермен ұғымдық шатасуға болмайды. Мұндай мәндер үшін біз T = предикат(дұрыс) және F = предикат(жалған) болатындай түр өзгертуді жүзеге асыруымыз керек. Мұндай өзгерту көбінесе жеңіл-жеңіл жасалады, сондықтан адамдар T-ны дұрыс, ал F-ны жалған деп қабылдауға бейім.

Детерминистік емес қорғалған командалар

Шындығында, Дикстраның күзетілген команда тілі (GCL) – бұл осы уақытқа дейін қарастырылған қарапайым императивті тілдің детерминистік емес операторлармен толықтырылған нұсқасы. Расында, GCL алгоритмдерді формалды түрде беруге арналған. Детерминистік емес операторлар – нақты іске асыру кезінде (тиімді бағдарламалау тілінде) таңдау жасау мүмкіндігін білдіреді: детерминистік емес операторлар үшін дәлелденген қасиеттер, іске асырудың барлық мүмкін нұсқалары үшін сақталады. Яғни, детерминистік емес операторлардың ең әлсіз алғышарттары, аяқталуға келетін орындалудың бар екенін (мысалы, іске асырудың бар екенін) және аяқталуға келетін барлық орындалулардың соңғы күйі пост-шартты қанағаттандыратынын қамтамасыз етеді. Жоғарыда келтірілген ең әлсіз алғышарттардың анықтамасы (әсіресе while циклы үшін) осы қасиетті сақтайды екенін есте сақтаңыз.

Қайталау

Қайталау - while операторының ұқсас түріндегі жалпылауы.

Win және sin предикаттық трансформаторлары

Лесли Лэмпорт бір мезгілде бағдарламалау үшін «win» және «sin» предикаттарын түрлендіргіштер ретінде ұсынған.

Предикаттық трансформаторлардың қасиеттері

Бұл бөлімде предикат трансформаторларының ерекше қасиеттері қарастырылады. Төменде S – күй кеңістігіндегі екі предикат арасындағы функция болып табылатын предикат трансформаторын, ал P – предикатты білдіреді. Мысалы, S(P) wp(S,P) немесе sp(S,P) деп таңбалануы мүмкін. Біз x-ті күй кеңістігінің айнымалысы ретінде қолдана береміз.

Монотонды

Баяндамалық трансформаторлар (wp, wlp және sp) монотонды. Предикат трансформаторы S монотонды, егер және тек егер:

Бұл қасиет Хоар логикасының салдар ережесімен байланысты.

Қолданбалар

Ең әлсіз алғышарттарды есептеу теореманы дәлелдейтін құралдарды (SMT шешушілер немесе дәлелдеуге көмектесетін жүйелер сияқты) қолдана отырып, бағдарламалардағы талаптарды статикалық түрде тексеру үшін кеңінен қолданылады: мысалы, Frama C немесе ESC/Java2. Көптеген басқа семантикалық формализмдерден өзгеше, предикат түрлендіру семантикасы есептеудің негіздерін зерттеу мақсатымен жасалмаған. Керісінше, ол бағдарламашыларға бағдарламаларын "есептеу стилінде" "құрылысымен дұрыс" деп дамытуға мүмкіндік беретін әдістеме ұсынуды көздеген. Бұл "жоғарыдан төменге" стильді Дикстра және Н. Вирт қолдаған. Оны Р. Дж. Бэк және басқалар тазарту есептеуінде одан әрі формалдаған. B әдісі сияқты кейбір құралдар осы әдістемені қолдау үшін автоматтандырылған қорытуды ұсынады. Хоар логикасының метатеориясында ең әлсіз алғышарттар салыстырмалы толықтықты дәлелдеудегі маңызды түсінік ретінде қарастырылады.

Императивті өрнектердің ең әлсіз алғышарттары мен ең күшті кейінгі шарттары

Предикат түрлендіргіштер семантикасында өрнектер логиканың терминдерімен шектеледі (жоғарыда қараңыз). Дегенмен, бұл шектеу көптеген қолданыстағы бағдарламалау тілдері үшін тым қатаң болып көрінеді, себебі өрнектер жанама әсерлерге ие болуы мүмкін (жанама әсері бар функцияны шақыру), аяқталмауы немесе қатемен тоқтауы мүмкін (мысалы, нөлге бөлу). Императивті өрнек тілдері үшін, әсіресе монадтар үшін ең әлсіз алғышарттарды немесе ең күшті постшарттарды кеңейту бойынша көптеген ұсыныстар жасалған. Олардың арасында Хоардың типтік теориясы Хаскелл сияқты тіл үшін Хоар логикасын, ажырату логикасын және типтік теорияны біріктіреді. Бұл жүйе қазіргі уақытта Ynot деп аталатын Coq кітапханасы ретінде жүзеге асырылған. Бұл тілде өрнектерді бағалау ең күшті посткондицияларды есептеуге сәйкес келеді.