Correctness_Algebras.Pre_Post