Figure:
Hoare
logic
Open figure
