# jlouis/janus-formalization

Page 23 done.

 @@ -14,13 +14,13 @@ \chapter{Full JANUS} introduced with notation $\rho |=_{loop} \angel{\sigma, (e_1, s_1, s_2, e_2)} -> \sigma'$. This states the evaluation of the loop identified by the quadruple $(e_1, s_1, s_2, e_2)$ under the function -definition $\rho$ and the store $\sigma$ will yield an updated store +environment $\rho$ and the store $\sigma$ will yield an updated store $\sigma'$. We then alter the judgement rules of statements by the following looping rule: \begin{equation*} - \inference[Loop]{\sigma |- e_1 => k \quad k \neq 0 \\ + \inference[Loop]{\sigma |- e_1 => \lift{k} \quad k \neq 0 \\ \rho |= \angel{\sigma, s_1} -> \sigma'' \quad \rho |=_{loop} \angel{\sigma'', (e_1, s_1, s_2, e_2)} -> \sigma'} {\rho |= \angel{\sigma, \ e \ s \ s \ e} -> \sigma'} @@ -33,7 +33,7 @@ \chapter{Full JANUS} \cite{yokoyama.axelsen.ea:principles}. The first one exits the loop then the until'' part evaluates to true: \begin{equation*} - \inference[LpT]{\sigma |- e_2 => k \quad k \neq 0} + \inference[LpT]{\sigma |- e_2 => \lift{k} \quad k \neq 0} {\rho |=_{loop} \angel{\sigma, (e_1, s_1, s_2, e_2)} -> \sigma} \end{equation*} Finally, if the until'' part evaluates to false, we take another
 @@ -316,7 +316,7 @@ \section{Determinism properties of \januso{}} \januso{} is backward deterministic, ie: \begin{equation*} \forall \sigma, \sigma', \sigma'' \in \Sigma, s \in Stm \colon - \rho |= \angel{\sigma', s} -> \sigma \implies \rho |= \angel{\sigma'', s} -> \sigma \implies \sigma' = \sigma'' + \rho |= \angel{\sigma', s} -> \sigma => \rho |= \angel{\sigma'', s} -> \sigma => \sigma' = \sigma'' \end{equation*} \end{thm} \begin{proof} @@ -327,8 +327,8 @@ \section{Inversion and its properties} Inverting \januso{} works exactly like inverting \janusz{}. We only need to add a couple of new rules for $\$ and $\$ and -the $\hat{=}$ operation. The two call types are each others inverses -and the $\$ operation is self inverse: +the $\hat{=}$ operation. The $\$ and $\$ statements are +each others inverses and the $\$ operation is self inverse: \begin{align*} \mathcal{I}(x \;\hat{=}\; e)& = x \;\hat{=}\; e\\ \mathcal{I}(\ p)& = \ p\\ @@ -345,7 +345,10 @@ \section{Inversion and its properties} \rho |= \angel{\sigma, s} -> \sigma' \iff \rho |= \angel{\sigma', \mathcal{I}(s)} -> \sigma \end{equation*} \end{thm} - +\begin{proof} + By \coq{}. The proof can be completed by straightforward extension of the + same proof for \janusz{}. +\end{proof} %%% Local Variables: