Формальное определение вызова процедуры

Формальное определение вызова процедуры

, :=, ;   B ; ,:=, .

Wp(“p()”,R)=wp(“, :=, ; B; ,:=, . ”,R)

Теорема 1 (о вызове процедуры)

Proc P(value, value result, result  )

{P}  B  {Q}        //B: , :=,   сокращено тело

{PR: P Ù (", :Q Þ R)}

     P(,,)

Рекомендуемые материалы

{R}

PRÞwp(p(,,),R)

PR можно использовать в качестве предусловия.

Пример:   , = ,

Proc swap (value result y₁, y₂);

{P: y₁=X Ù y₂=Y}

     B

{Q: y₁=Y Ù y₂=X }

Доказать, что если {a=X Ù b=Y} то после вызова процедуры swap (a,b) будет

{a=Y, b=X}

Доказательство:

PR = (a=X Ù b=Y Ù (" u₁,u₂: Q: u₁=Y Ù u₂=X Þ u₁=Y Ù u₂=X)) = a=X Ù b=Y

Пример:

{a=A Ù b=B} – предусловие, та же процедура swap(a,b)

{a=B Ù b=A}

{y₁=X Ù y₂=Y} B {y₁=Y Ù y₂=X} = {y₁=A Ù y₂=B} B {y₁=B Ù y₂=A}

Пример:

{i=I Ù(" k: b[k]=B[k])}

     swap(i, b[i])

{i:=B[I] Ù B[I]=I Ù "k : I¹k : b[k]=B[k]}

Перепишем процедуру

Вам также может быть полезна лекция "Введение в вычислительные сети".

{P: y₁=I Ù y₂=B[I]} y₁,y₂:=u₁,u₂ {Q: y₁=B[I] Ù y₂=I}

     PR=PÙ(" u₁,u₂ Q Þ R) =

= i=I Ù b[i]=B[I] Ù (" u₁,u₂ u₁=B[I] Ù u₂=I Þ

Þ u₁=B[I] Ù (b:i:u₂)[I]=I Ù "k¹(b:i:u₂)[k]=B[k])= //раскроем квантор всеобщности

= i=I Ù b[i]=B[I] Ù (B[I]=B[I] Ù I=I Þ B[I]=B[I] Ù

Ù (b:i:I)[I]=I Ù "k:k¹I:(b:i:I)[k]= B[k])Þ( i=I Ù b[i]=B[I] Ù I=I Ù "k: k¹I:b[k]B[k])=i=I Ù ("k: b[k]=B[k])