In the previous section, I’ve given a formal definition of the programming language that I’ve been trying to analyze. This formal definition serves as the “ground truth” for how our little imperative programs are executed; however, program analyses (especially in practice) seldom take the formal semantics as input.
