Finally, the specifications are expressed as assertions. The program segment transform these assertions. If the assertion A holds before the execution of the program P, on termination of P, assertion B holds after the execution of P.

---