Верификация - Теория вычислительных процессов

1. Без ветвлений:

A) mov di,1

Mov al, adg

Add di, ax

Mov al, buf1[di]

Mov ah, buf2[di]

Sbb al, ah

TRUE

B) mov dl, buf1[di]

Mov bl, buf2[di]

Mov buf1[di],bl

Mov buf2[di],dl

TRUE {dl=buf1[di] ,bl=buf2[di] ,buf1[di]=bl, buf2[di]=dl}

(buf1[di]= buf2[di]( buf2[di]= buf1[di])

TRUE {dl=buf1[di] , bl=buf2[di] , buf1[di]=bl}

(buf1[di]= buf2[di])( dl= buf1[di])

TRUE { dl=buf1[di] , bl=buf2[di]}

(bl= buf2[di])( dl= buf1[di])

TRUE { dl=buf1[di]}

(buf2[di]= buf2[di])( dl= buf1[di])

TRUE (buf2[di]= buf2[di])( buf1[di]= buf1[di])

TRUE TRUE

TRUE

TRUE TRUE

TRUE

2. С ветвлением:

A) cmp flagbuf1,1

Je FirstNum

Jne SecondNum

FirstNum:

Mov Sign1,1

...

Jmp EndPerev

SecondNum:

Mov Sign2,1

...

Jmp EndPerev

EndPerev:

...

Для доказательства того, что

(flagbuf1=1)(flagbuf1=0)

{ if flagbuf1=1 then Sign1:=1 else Sign2:=1}

(Sign1=1Sign2=1)

Необходимо доказать три условия истинности:

    1) без побочных эффектов (flagbuf1=1) 2) ((flagbuf1=1)(flagbuf1=0)) &; (flagbuf1=1) {Sign1:=1} (Sign1=1Sign2=1) ((flagbuf1=1)(flagbuf1=0)) &; (flagbuf1=1) ( 1=1 Sign2=1)

True True

True

    3) ((flagbuf1=1)(flagbuf1=0)) &; (flagbuf1=0) {Sign2:=1} (Sign1=1Sign2=1) ((flagbuf1=1)(flagbuf1=0)) &; (flagbuf1=0) (Sign1=1 1=1)

True True

True

B) mov di,2

Mov cl, adg

LViv:

Mov al, buf3[di]

Inc di

...

Loop LViv

В этом примере является инвариантом.

Для доказательства того, что

Покажем, что цикл всегда завершается, и продемонстрируем истинность следующих утверждений:

    1. Инвариант цикла удовлетворяется при входе в цикл, т. е. предусловие включает в себя инвариант: 2. Если инвариант истинен перед вычислением предиката управляющим циклом, то он истинен после его вычисления:

Т. к. вычисление свободно от побочных эффектов, то входное условие на рушиться не может, следовательно, утверждение истинно.

3. Инвариант цикла удовлетворяется в теле цикла:

True

4. Инвариант цикла и отрицание условия выполнения имплицируют постусловие:

True

Похожие статьи




Верификация - Теория вычислительных процессов

Предыдущая | Следующая