Describir: Logica de hoare para programas concurrentes