Fix the Janus0 definition.

jlouis · Apr 12, 2009 · eb25862 · eb25862
1 parent 7a550c3
commit eb25862
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Janus0.v b/Janus0.v
@@ -99,7 +99,7 @@ Section Janus0.
     | se_assvar_decr: forall (m m': mem) (v: Var) (z z' r: Z) (e: Exp),
       denote_Exp (ZMem.hide m v) e = Some z ->
       m v = Some z' ->
-      r = (z - z') ->
+      r = (z' - z) ->
       m' = ZMem.write m v r ->
       Stm_eval m (S_Decr v e) m'
     | se_semi: forall (m m' m'': mem) (s1 s2: Stm),