Detecting Common Mode Failures in N-Version Software Using Weakest Precondition Analysis