This is how predicate transformer semantics views programs. An executing procedure is a walk through the program state space.
For example an instance of a struct with n fields is a point in an n-dimensional state space. A method that modifies that struct is moving that instance through that space. Where this gets cool is that it's possible to prove that for all points in the state space, a given program will reliably establish a defined postcondition.
To give a trivial example, imagine a state space with a few billion variables. Let's suppose one of those variables is called x and we want to establish the postcondition x = 0.
x := 0
The above program will establish x == 0 regardless of the initial state and we don't need to worry about the several billion other dimensions in the state space. To a mathematician I imagine this is immensely boring, but for a working software developer boring is great, because it's so easy to otherwise build cognitively unmanageable systems.
For example an instance of a struct with n fields is a point in an n-dimensional state space. A method that modifies that struct is moving that instance through that space. Where this gets cool is that it's possible to prove that for all points in the state space, a given program will reliably establish a defined postcondition.
To give a trivial example, imagine a state space with a few billion variables. Let's suppose one of those variables is called x and we want to establish the postcondition x = 0.
The above program will establish x == 0 regardless of the initial state and we don't need to worry about the several billion other dimensions in the state space. To a mathematician I imagine this is immensely boring, but for a working software developer boring is great, because it's so easy to otherwise build cognitively unmanageable systems.