Computing differs from math by its dependence on state changes, among other things. A program can be seen as a composition of state transitions, and it would be nice to have an inverse function to map a program text back to mathematics. You might also compare with transformations caused by changes of coordinate system. So:

How does one argue mathematically about equality of one expression's value in state $\sigma_{i+1}$ to another's in state $\sigma_i$, i.e. $\sigma_i(E)=\sigma_{i+1}(E')$, and relate it to properties of the state transition $\sigma_i\mapsto\sigma_{i+1}$?

Do not just refer to functional programming, because it circumvents the need to discuss state changes. I am familiar with it and have reasons to look for alternatives.

Specifically I would like to argue in terms of informal expressions like $f(S)(\sigma)(\lambda \nu.E)$ with $S$ varying over program expressions, $\sigma$ over states, and both $\nu$ and $E$ over expressions. Similar expressions are used for model-based semantics of programming languages, only with $\lambda \nu.E$ as a notation for an ordinary function (i.e. with $\nu$ varying over a domain of values).

The problem concerns arguing about an expression, rather than its interpretation 'in any state'. Is it appropriate to talk about functions with a domain of expressions? Differential and integral calculus concern expressions, but still presumes a fixed state. I am looking for a foundation for sound arguments when a current state changes, as in programming with assignments.

E.W. Dijkstra's transformation rules for a predicate valid in state $\sigma_{i+1}$ back to a predicate valid in state $\sigma_i$ is an attempt of the kind I'm looking for. His transformations depends on substitution of a program expression into a mathematical expression -- which is not generally acceptable.