UTP semantics of non-deterministic side-effecting expression

C programming language is safety-critical, in order to reduce the problems caused by its loose semantics, we are going to use Unifying Theories of Programming framework to give a semantics to an imperative language with global variables, side-effecting functions, and arbitrary sub-expression reordering, and then use this to explore how to formally define “safety”. The main technology roadmap we use in this paper is to first find out a set of new semantics and then check the healthiness of eleven basic laws, then use those laws to check the healthiness of our new semantics to see if they match the prescript healthiness conditions, then we do some work to make the previous semantics better. The most important ways of doing proofs are from the module Formal Methods and many ideas related to First-order predicate calculus. At last, we gained a new semantics and definitions of syntax successfully though there is still a long way to go.