Mazdak Farrokhzad edited Rules.tex  over 9 years ago

Commit id: c9581f6f22217216b394a3f650fe71f12771f51d

deletions | additions      

       

\begin{equation}  \begin{split}  \wp{x :=e}{R} &= R[x \mapsto e] & &&  \rule{1}\\ \wp{S1; S2}{R} &= \wp{S1}{\wp{S2}{R}} & &&  \rule{2}\\ \wp{\mtt{assert }B}{R} &= B \a R & &&  \rule{3}\\ \wp{\ie{B}{S1}{S2}}{R} &= B \to \wp{S1}{R} \a \neg B \to \wp{S2}{R} & &&  \rule{4}\\ \wp{\if{B}{S1}}{R} &= B \to \wp{S1}{R} \a \neg B \to R & &&  \rule{5}\\ \end{split}  \end{equation}