this is for holding javascript data
Mazdak Farrokhzad edited Rules.tex
over 9 years ago
Commit id: 32fb97b6a820f0a93c524113a212a28d763eebdd
deletions | additions
diff --git a/Rules.tex b/Rules.tex
index 8faffeb..3898b80 100644
--- a/Rules.tex
+++ b/Rules.tex
...
\begin{equation}
\begin{split}
\wp{x :=e}{R} &= R[x \mapsto e] & \mbb{Assignment,
R#1}\\ §1}\\
\wp{S1; S2}{R} &= \wp{S1}{\wp{S2}{R}} & \mbb{Sequential,
R#2}\\ §2}\\
\wp{\mtt{assert }B}{R} &= B \a R & \mbb{Assertion,
R#3}\\ §3}\\
\wp{\ie{B}{S1}{S2}}{R} &= B \to \wp{S1}{R} \a \neg B \to \wp{S2}{R} & \mbb{Conditional,
R#4}\\ §4}\\
\wp{\if{B}{S1}}{R} &= B \to \wp{S1}{R} \a \neg B \to R & \mbb{Conditional,
R#5}\\ §5}\\
\end{split}
\end{equation}