Editing Hoare logic (section)

===Rule of composition===

{| align=right class="wikitable collapsible collapsed"
|-
! Verifying swap-code<BR>without auxiliary variables
|-
|
{| style="border:1px solid grey;"
|+ The three statements below (line 2, 4, 6) exchange the values of the variables {{mvar|a}} and {{mvar|b}}, without needing an auxiliary variable. In the verification proof, the initial value of {{mvar|a}} and {{mvar|b}} is denoted by the constant {{mvar|A}} and {{mvar|B}}, respectively. The proof is best read backwards, starting from line 7; for example, line 5 is obtained from line 7 by replacing {{mvar|a}} (target expression in line 6) by <math>a-b</math> (source expression in line 6). Some arithmetical simplifications are used tacitly, viz. <math>a-(a-b) = b</math> (line 5→3), and <math>a+b-b = a</math> (line 3→1).
|-
| '''Nr''' || '''Code''' || COLSPAN=6 | '''Assertions'''
|-
| '''1:''' &nbsp; &nbsp; &nbsp; || || <math>\{a  = A \wedge b = B \}</math>
|-
| '''2:''' || <math>a := a + b;</math> &nbsp; &nbsp; &nbsp; 
|-
| '''3:''' || || <math>\{ a - b = A \wedge b = B \}</math>
|-
| '''4:''' || <math>b := a - b;</math>
|-
| '''5:''' || || <math>\{b=A\wedge a-b=B\}</math>
|-
| '''6:''' || <math>a := a - b</math>
|-
| '''7:''' || || <math>\{b= A\wedge a = B \}</math>
|}
|}
Hoare's rule of composition applies to sequentially executed programs {{mvar|S}} and {{mvar|T}}, where {{mvar|S}} executes prior to {{mvar|T}} and is written <math>S;T</math> ({{mvar|Q}} is called the ''midcondition''):{{sfn|Huth|Ryan|2004}}

:<math>\dfrac{\{P\} S \{Q\}\quad,\quad   \{Q\} T \{R\}}{\{P\} S;T \{R\}}</math>

For example, consider the following two instances of the assignment axiom:

:<math>\{ x + 1 = 43 \}   y := x + 1   \{ y = 43 \}</math>

and

:<math>\{ y = 43 \}   z := y   \{ z = 43 \}</math>

By the sequencing rule, one concludes:

:<math>\{ x + 1 = 43 \}   y := x + 1; z := y   \{ z = 43 \}</math>

Another example is shown in the right box.