4 ms·
No you can't. You can claim that your spec doesn't violate some invariants in a finite number of steps, you can't claim that the spec contains all the invarian
by llm_trw 3y ago
No you can't.
You can claim that your spec doesn't violate some invariants in a finite number of steps, you can't claim that the spec contains all the invariants the real system must have and that it doesn't violate them in number of steps + 1.