Invariância

Propriedades de invariância são demonstradas por indução , ou seja, para mostrar que P é um invariante, devemos mostrar que

1.: P é válido inicialmente
2.: toda operação sobre a estrutura de dados compartilhada que se inicia com P válido deixa P válido

Por ``operação'' deve ser entendida toda modificação feita com a posse da chave.

A construção while (condition) do wait(b,k) simplifica muito este raciocínio indutivo.