Rewriting system.

sireum · Mar 8, 2024 · 676f98f · 676f98f
1 parent a99065b
commit 676f98f
Show file tree

Hide file tree

Showing 3 changed files with 135 additions and 46 deletions.
diff --git a/jvm/src/test/scala/org/sireum/logika/example/rewrite.sc b/jvm/src/test/scala/org/sireum/logika/example/rewrite.sc
@@ -31,9 +31,9 @@ import Rules._
   Deduce(
     (2 * c + 3 * c == d) |- (5 * c == d) Proof(
       //@formatter:off
-      1  (2 * c + 3 * c == d)  by Premise,
-      2  (5 * c == d)          by Rewrite(RS(zDistribute _), 1) T,
-      3  (5 * c == d)          by Rewrite(myRewriteSet, 1) T
+      1 (  2 * c + 3 * c == d  ) by Premise,
+      2 (  5 * c == d          ) by Rewrite(RS(zDistribute _), 1) T,
+      3 (  5 * c == d          ) by Rewrite(myRewriteSet, 1) T
       //@formatter:on
     )
   )
@@ -43,9 +43,9 @@ import Rules._
   Deduce(
     (c ≡ d, (c + 1) ≡ 3) |- ((d + 1) ≡ 3) Proof(
       //@formatter:off
-      1  (c ≡ d)              by Premise,
-      2  ((c + 1) ≡ 3)        by Premise,
-      3  ((d + 1) ≡ 3)        by Simpl //Rewrite(RS(subst[Z] _), 2)
+      1 (  c ≡ d        ) by Premise,
+      2 (  (c + 1) ≡ 3  ) by Premise,
+      3 (  (d + 1) ≡ 3  ) by Simpl //Rewrite(RS(subst[Z] _), 2)
       //@formatter:on
     )
   )
@@ -55,9 +55,9 @@ import Rules._
   Deduce(
     (c ≡ d, (d + 1) ≡ 3) |- ((c + 1) ≡ 3) Proof(
       //@formatter:off
-      1  (c ≡ d)              by Premise,
-      2  ((d + 1) ≡ 3)        by Premise,
-      3  ((c + 1) ≡ 3)        by Rewrite(~RS(subst[Z] _), 2) and (1, 2) // and (...) is optional but it makes the search faster
+      1 (  c ≡ d        ) by Premise,
+      2 (  (d + 1) ≡ 3  ) by Premise,
+      3 (  (c + 1) ≡ 3  ) by Rewrite(~RS(subst[Z] _), 2) and (1, 2) // and (...) is optional but it makes the search faster
       //@formatter:on
     )
   )
@@ -68,36 +68,36 @@ import Rules._
 @pure def binaryConstantPropagation(): Unit = {
   Deduce(
     //@formatter:off
-    1  (1 + 2 == 3)  by Simpl
+    1 (  1 + 2 == 3  ) by Simpl
     //@formatter:on
   )
 }
 
 @pure def unaryConstantPropagation(): Unit = {
   Deduce(
     //@formatter:off
-    1  (-(-1) == 1)  by Simpl
+    1 (  -(-1) == 1  ) by Simpl
     //@formatter:on
   )
 }
 
 @pure def fieldAccess(o: EvalFoo[Z, Z]): Unit = {
   Deduce(
     //@formatter:off
-    1  (EvalFoo(x = 4, y = 5).x == 4)   by Simpl,
-    2  (o(x = 4, y = 5).x == 4)         by Simpl,
-    3  (o(x = 4, y = 5).y == 5)         by Simpl,
-    4  (o(x = 4)(y = 1)(x = 5).x == 5)  by Simpl,
-    5  (o(x = 4)(x = 5).y == o.y)       by Simpl
+    1 (  EvalFoo(x = 4, y = 5).x == 4   ) by Simpl,
+    2 (  o(x = 4, y = 5).x == 4         ) by Simpl,
+    3 (  o(x = 4, y = 5).y == 5         ) by Simpl,
+    4 (  o(x = 4)(y = 1)(x = 5).x == 5  ) by Simpl,
+    5 (  o(x = 4)(x = 5).y == o.y       ) by Simpl
     //@formatter:on
   )
 }
 
 @pure def tupleProjection(): Unit = {
   Deduce(
     //@formatter:off
-    1  ((1, 2)._1 == 1)   by Simpl,
-    2  ((1, 2)._2 == 2)   by Simpl
+    1 (  (1, 2)._1 == 1  ) by Simpl,
+    2 (  (1, 2)._2 == 2  ) by Simpl
     //@formatter:on
   )
 }
@@ -108,13 +108,13 @@ import Rules._
   )
   Deduce(
     //@formatter:off
-    1  (i != j)                             by Premise,
-    2  (i == k)                             by Premise,
-    3  (ISZ(1, 2, 3).size == 3)             by Simpl,
-    4  (ISZ[Z](1, 2, 3)(0 ~> 5).size == 3)  by Simpl,
-    5  (a(0 ~> t1).size == a.size)          by Simpl,
-    6  (a(i ~> t1)(j ~> t2)(i) == t1)       by Simpl,
-    7  (a(i ~> t1)(k ~> t2)(i) == t2)       by Simpl
+    1 (  i != j                             ) by Premise,
+    2 (  i == k                             ) by Premise,
+    3 (  ISZ(1, 2, 3).size == 3             ) by Simpl,
+    4 (  ISZ[Z](1, 2, 3)(0 ~> 5).size == 3  ) by Simpl,
+    5 (  a(0 ~> t1).size == a.size          ) by Simpl,
+    6 (  a(i ~> t1)(j ~> t2)(i) == t1       ) by Simpl,
+    7 (  a(i ~> t1)(k ~> t2)(i) == t2       ) by Simpl
     //@formatter:on
   )
 }
@@ -125,7 +125,7 @@ import Rules._
 @pure def incNTest(a: Z): Unit = {
   Deduce(
     //@formatter:off
-    1  (a + 1 == incN(a, 1))                 by Simpl
+    1 (  a + 1 == incN(a, 1)  ) by Simpl
     //@formatter:on
   )
 }
@@ -136,7 +136,7 @@ import Rules._
 @pure def incTest(a: Z): Unit = {
   Deduce(
     //@formatter:off
-    1  (a + 1 == inc(a))                     by RSimpl(RS(inc _))
+    1 (  a + 1 == inc(a)  ) by RSimpl(RS(inc _))
     //@formatter:on
   )
 }
@@ -147,8 +147,18 @@ import Rules._
   )
   Deduce(
     //@formatter:off
-    1  (a + b + (3 - 1) > 3)                  by Premise,
-    2  (a + b + 2 > 3)                        by Eval(1)
+    1 (  a + b + (3 - 1) > 3  ) by Premise,
+    2 (  a + b + 2 > 3        ) by Eval(1)
     //@formatter:on
   )
 }
+
+@pure def labelTest(a: Z): Unit = {
+  Contract(
+    Requires(a + (3 - 2) > inc(5 * 2))
+  )
+  Deduce(
+    1 (  a + (3 - 2) > (inc(5 * 2): @l)  ) by Premise,
+    2 (  a + (3 - 2) > 11                ) by Rewrite(RS(inc _), 1)
+  )
+}