(* 2-sort3.ec *) (* sort three integers *) prover ["Z3"]. require import AllCore List. (* perm3 (x, y, z) (x', y', z') tests whether there is there is a way of permuting (x', y', z') so as to get (x, y, z) *) op perm3 (u : int * int * int) (u' : int * int * int) : bool = let (x, y, z) = u in let (x', y', z') = u' in (x, y, z) = (x', y', z') \/ (x, y, z) = (x', z', y') \/ (x, y, z) = (y', x', z') \/ (x, y, z) = (y', z', x') \/ (x, y, z) = (z', x', y') \/ (x, y, z) = (z', y', x'). module M = { var x, y, z : int var x', y', z' : int (* inputs: x y z outputs: x' y' z' *) proc sort3() : unit = { if (x <= y) { if (y <= z) { x' <- x; y' <- y; z' <- z; } else { if (x <= z) { x' <- x; y' <- z; z' <- y; } else { x' <- z; y' <- x; z' <- y; } } } else { if (x <= z) { x' <- y; y' <- x; z' <- z; } else { if (y <= z) { x' <- y; y' <- z; z' <- x; } else { x' <- z; y' <- y; z' <- x; } } } } }. lemma sort3 (x_ y_ z_ : int) : hoare[M.sort3 : M.x = x_ /\ M.y = y_ /\ M.z = z_ ==> M.x' <= M.y' <= M.z' /\ perm3 (x_, y_, z_) (M.x', M.y', M.z')]. proof. proc. if. if. wp; skip; progress. if. wp; skip; progress; smt(). wp; skip; progress; smt(). if. wp; skip; progress; smt(). if. wp; skip; progress; smt(). wp; skip; progress; smt(). qed. (* we didn't advertise that wp can also handle these nested if statements, so that a shorter proof is possible: *) lemma sort3' (x_ y_ z_ : int) : hoare[M.sort3 : M.x = x_ /\ M.y = y_ /\ M.z = z_ ==> M.x' <= M.y' <= M.z' /\ perm3 (x_, y_, z_) (M.x', M.y', M.z')]. proof. proc. wp; skip; smt(). qed.