Mazdak Farrokhzad edited Rules.tex  over 9 years ago

Commit id: 780eb467e033227f19d93c38b8ad2db0c2972807

deletions | additions      

       

\newcommand{\mbb}[1]{\mathbf{#1}}  \newcommand{\T}[0]{\mbb{\top}}  \newcommand{\F}[0]{\mbb{\bot}}  \newcommand{\rule}[1]{\mbb{§#1}}  \begin{equation}  \begin{split}  \wp{x :=e}{R} &= R[x \mapsto e] & \mbb{Assignment, §1}\\ \rule{1}\\  \wp{S1; S2}{R} &= \wp{S1}{\wp{S2}{R}} & \mbb{Sequential, §2}\\ \rule{2}\\  \wp{\mtt{assert }B}{R} &= B \a R & \mbb{Assertion, §3}\\ \rule{3}\\  \wp{\ie{B}{S1}{S2}}{R} &= B \to \wp{S1}{R} \a \neg B \to \wp{S2}{R} & \mbb{Conditional, §4}\\ \rule{4}\\  \wp{\if{B}{S1}}{R} &= B \to \wp{S1}{R} \a \neg B \to R & \mbb{Conditional, §5}\\ \rule{5}\\  \end{split}  \end{equation}