Доказательство правильности - это подтверждение того, что семантика программы соответствует предъявляемым требованиям, изложенным в спецификации этой программы. Существуют два предварительных условия для построения такого доказательства: необходимо иметь формальное описание программы и формальное определение используемого языка программирования. Такое определение может принимать фирму системы аксиом, охватывающих семантические правила для любого простого оператора в языке, и набора правил вывода, показывающих, как семантики составных операторов к числу которых относится и целостная программа.

Интерпретированные пооперационно утверждения характеризуют состояние программы. Доказательство строится на следующей схеме: если выполнение программы начинается в состоянии, когда входное утверждение истинно, то работа программы в итоге должна завершаться состоянием, при котором выходное утверждение тоже истинно. Этот тип доказательства известен как доказательство общей правильности. Традиционно, однако, такое доказательство часто выполняется в два этапа. Вначале доказывается правильность частей программы (частичная правильность); считается, что, если программа завершается нормально, то это происходит в состоянии, для которого выходное утверждение истинно. На втором этапе доказывается правильность завершения программы; в результате этого доказательства показывается, что программа завершила работу нормально, а не преждевременно.

Совместимость семантики с предусловием и постусловием.

Описание программы может очень удобно представляться в форме двух утверждений: входного и выходного. Для того чтобы проверить правильность программы, необходимо сформулировать предусловие – выражение, определяющее значение до начала работы группы операторов и постусловие – выражение, определяющее значение после окончания работы группы операторов.

Если выражение на входе и на выходе соответствует ожидаемому, то группу операторов можно считать семантически правильной. Для доказательства правильности циклических участков в ней включают так называемые инварианты циклов. Инвариант- это утверждение, которое остается истинным при некотором преобразовании или отображении. При доказательстве правильности инвариантом является некоторое утверждение о свойствах фрагментов программы, который остается истинным не смотря выполненную часть этого аргумента. Инвариант цикла – выражение, значение которого не изменяется при каждом прохождении цикла.

Для доказательства факта завершения программы необходимо доказать:

1)Что программа не зациклилась

2)Что программа не остановлена преждевременно