diff options
author | Carlo Zancanaro <carlo@pc-4w14-0.cs.usyd.edu.au> | 2012-11-26 20:18:42 +1100 |
---|---|---|
committer | Carlo Zancanaro <carlo@pc-4w14-0.cs.usyd.edu.au> | 2012-11-26 20:18:42 +1100 |
commit | ab443f619d207564e4972274c571ef15da70a74c (patch) | |
tree | 4d06e93e1f66b3c4e43b1de17557a96a56821823 /tex/thesis/litreview | |
parent | 7ad1aed1a3ba88e2c40c82da05b9bf35eedc4096 (diff) |
Thesis thesis thesis.
Diffstat (limited to 'tex/thesis/litreview')
-rw-r--r-- | tex/thesis/litreview/litreview.tex | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tex/thesis/litreview/litreview.tex b/tex/thesis/litreview/litreview.tex index 109864e..38bd9dc 100644 --- a/tex/thesis/litreview/litreview.tex +++ b/tex/thesis/litreview/litreview.tex @@ -8,7 +8,7 @@ \newcommand{\Stmt}{\mathsf{Stmt}} \newcommand{\Vars}{\mathsf{Vars}} -\chapter{Preliminaries} \label{chap:litreview} +\chapter{Background} \label{chap:litreview} In this chapter we review the relevant literature pertaining to static analysis. We briefly cover the semantics of programs generally before @@ -38,9 +38,9 @@ side-effects, so it is necessary to introduce some notion of ``state'' into our semantics. By defining $\semantics{\cdot}: \states \to \states$ for all statements $x$ we provide a mechanism for statements to perform side effects. Elements of $\states$ each represent a -possible state for the program to be in. For example: for an -integral assignment statement $I := E$, assigning the value of an -expression $E$ to a variable $I$, have the following denotation: +possible state for the program to be in. For example: for an integral +assignment statement $I := E$, assigning the value of an expression +$E$ to a variable $I$, we have the following denotation: \begin{align*} \semantics{I := E} = \lambda \rho . (\rho \oplus \{I \mapsto \semantics{E}(\rho)\}) \end{align*} |