I'm a fan of more formal methods in progam analysis, but this particular excercise is very hindsight-is-20/20
> In this case, we can set up an invariant stating that the DNS should never be deleted once a newer plan has been applied
If that invariant had been expressed in the original code — as I'm sure it now is — it wouldn't have broken in the first place. The invariant is obvious in hindsight, but it's hardly axiomatic.
> In this case, we can set up an invariant stating that the DNS should never be deleted once a newer plan has been applied
If that invariant had been expressed in the original code — as I'm sure it now is — it wouldn't have broken in the first place. The invariant is obvious in hindsight, but it's hardly axiomatic.