Генератор условий проверки

Генератор условий проверки — это общий подкомпонент автоматического средства проверки программы , который синтезирует формальные условия проверки путем анализа исходного кода программы с использованием метода, основанного на логике Хоара . Генераторы VC могут потребовать, чтобы исходный код содержал логические аннотации, предоставленные программистом или компилятором, такие как предварительные и постусловия и инварианты цикла (форма кода, несущего доказательства ). Генераторы VC часто сочетаются с решателями SMT в серверной части верификатора программы. После того как генератор условий проверки создал условия проверки, они передаются автоматизированному средству доказательства теорем , которое затем может формально доказать правильность кода.

Предложены методы использования операционной семантики машинных языков для автоматического формирования генераторов условий проверки.