Тексеру жағдайы генераторы - Verification condition generator

A тексеру жағдайының генераторы автоматтандырылған жалпы қосалқы компонент болып табылады бағдарламаны тексеруші бағдарламаның бастапқы кодына негізделген әдісті қолдана отырып, тексерудің ресми шарттарын синтездейді Логика. VC генераторлары бастапқы кодтан бағдарламалаушы немесе компилятор ұсынған логикалық аннотацияларды талап етуі мүмкін, мысалы алдын-ала / кейінгі жағдайлар және цикл инварианттары ( дәлелдеуші коды ). VC генераторлары жиі біріктіріледі SMT еріткіштері бағдарлама тексерушісінің артында. Тексеру шартын жасағаннан кейін генератор тексеру шарттарын жасағаннан кейін олар an-ға беріледі автоматтандырылған теоремалық провер, содан кейін кодтың дұрыстығын ресми түрде дәлелдей алады.

Қолданудың әдістері ұсынылды жедел семантика Автоматты түрде тексеру шартының генераторларын құруға арналған машиналар тілдерінің.[1]

Әдебиеттер тізімі

  1. ^ Джон Мэттьюс; Дж. Стристер Мур; Сэндип Рэй; Дарон Врон (2005). «Теорема арқылы дәлелдеу шарттарын генерациялау». Мики Германда; Андрей Воронков (ред.). Proc. Int. Конф. Бағдарламалау, жасанды интеллект және пайымдау логикасы. LNCS. 4246. Спрингер. 362–376 беттер.