For computing there are three standard models for presenting semantics: axiomatic, denotational, and operational.
Axiomatic semantics was introduced by C. A. R. Hoare in the late 1960s and early 1970s. The basic unit of axiomatic semantics is the Hoare triple that we will write as {P}S{Q}. Informally, P is the precondition, S is the statement, and Q is the postcondition. The intent of this approach is to develop a logic similar to that used in ordinary mathematics.
The intuitive reading of {P}S{Q} is "If the state P is true and the statement S is executed, then the state Q obtains." Immediately, the issue arises, "Well, what if S doesn't terminate?" There is no unique answer to this question so there are two different interpretations of {P}S{Q}: (1) if P guarantees that S terminates then we have total correctness and (2) if P does not guarantee that S terminates we have partial correctness.
The major stumbling block in defining axiomatic semantics is that ordinary assignment is difficult to capture using this notation.
The major stumbling block in using axiomatic semantics has been the difficulty of using the notation to actually prove (in a mathematical sense) properties about programs.
For a language that you are familar with, choose a construct other than assignment and define its axiomatic semantics.