Refactoring Invariants

from blog Computer Things, | ↗ original
(Feeling a little sick so this one will be short.) I'm often asked by clients to review their (usually TLA+) formal specifications. These specs are generally slower and more convoluted than an expert would write. I want to fix them up without changing the overall behavior of the spec or introducing subtle bugs. To do this, I use a rather lovely...