|
|
|
|
|
by nicklaf
2762 days ago
|
|
If I understand exmadscientist correctly, this sounds a lot like Floyd's invariant principle, in which the argument is understood as mathematical induction, where the induction is on (property-preserving) transitions of the state machine (and with the initial state as base case). See section 2 of chapter 6 in Mathematics for Computer Science: https://courses.csail.mit.edu/6.042/spring18/mcs.pdf |
|