Correctness_Algebras.Preconditions