Slide 10.2: Applications of Hoare logic

Applications of Hoare Logic

Three examples of applications of Hoare logic are given next:

Given the assignment statement
```
   x := x + 1
```
we would expect that, whatever value x has just before execution of the statement, its value just after the execution of the assignment is one more than its previous value. This can be stated as the precondition that x = A before execution and the postcondition that x = A + 1 after execution:
```
   {x = A} x := x + 1 {x = A + 1}
```
The second example is
```
   {a > 0} a := a – 1 {a ≥ 0}
```
Consider the following assignment:
```
   x := 1/y
```
Clearly a precondition for the successful execution of the statement is that y ≠ 0, and then x becomes equal to 1/y. Thus we have
```
   {y ≠ 0} x := 1/y {x = 1/y}
```
or
```
   {y ≠ 0}
   x := 1/y
   {x = 1/y}
```
Note that in this example the precondition establishes a restriction that is a requirement for successful execution, while in the previous example the precondition x = A merely establishes a name for the value of x prior to execution, without making any restriction whatever on that value.