Step 1: Verification Condition Generation Procedure Reverse (updates S: List); decreasing |S.Right|; Var E: Entry; 0Assume: |S 0.Left| = 0; If Right_Length(S) > 0 then Remove(E, S); Reverse(S); Insert(E, S); end; 5Confirm: S 5.Left = S 0.Right Rev and S 5.Right = empty_string end Reverse;
{}