Skip to content

Commit 9b3bb98

Browse files
robby-phdrobby-phd
committed
@ induct support.
1 parent bb6b37f commit 9b3bb98

File tree

2 files changed

+27
-15
lines changed
  • jvm/src/test/scala/org/sireum/logika/example
  • shared/src/main/scala/org/sireum/logika

2 files changed

+27
-15
lines changed

‎jvm/src/test/scala/org/sireum/logika/example/list.sc

+24-14
Original file line numberDiff line numberDiff line change
@@ -89,7 +89,7 @@ object List {
8989
//@formatter:off
9090
1 ( l ≡ Cons(a, next) ) by Auto,
9191
2 ( next.length >= 0 ) by Premise,
92-
3 ( l.length ≡ (1 + next.length) ) by Simpl, // Auto,
92+
3 ( l.length ≡ (1 + next.length) ) by Auto,
9393
4 ( l.length >= 0 ) by Auto and (2, 3)
9494
//@formatter:on
9595
)
@@ -99,14 +99,24 @@ object List {
9999
Deduce(
100100
//@formatter:off
101101
1 ( l ≡ Nil[T]() ) by Auto,
102-
2 ( l.length >= 0 ) by Simpl // Auto
102+
2 ( l.length >= 0 ) by Auto
103103
//@formatter:on
104104
)
105105
return
106106
}
107107
}
108108
}
109109

110+
@pure def emptyZeroLengthInductExpansionTest[T](l: List[T]): Unit = {
111+
Contract(
112+
Ensures(l.length >= 0)
113+
)
114+
115+
l: @induct // to be expanded
116+
117+
halt("To be filled in")
118+
}
119+
110120
@pure def emptyZeroLengthInduct[T](l: List[T]): Unit = {
111121
Contract(
112122
Ensures(l.length >= 0)
@@ -356,8 +366,8 @@ object List {
356366
if (p._1 ≡ key2) {
357367
Deduce(
358368
//@formatter:off
359-
1 ( map ≡ Cons(p, next) ) by Premise, // Auto-generated
360-
2 ( lookup(update(next, key1, value), key2) ≡ lookup(next, key2) ) by Premise, // Auto-generated
369+
1 ( map ≡ Cons(p, next) ) by Premise, // auto-generated
370+
2 ( lookup(update(next, key1, value), key2) ≡ lookup(next, key2) ) by Premise, // auto-generated
361371
3 ( key1 ≢ key2 ) by Premise,
362372
4 ( !(p._1 ≡ key1) ) by Premise,
363373
5 ( p._1 ≡ key2 ) by Premise,
@@ -368,8 +378,8 @@ object List {
368378
} else {
369379
Deduce(
370380
//@formatter:off
371-
1 ( map ≡ Cons(p, next) ) by Premise, // Auto-generated
372-
2 ( lookup(update(next, key1, value), key2) ≡ lookup(next, key2) ) by Premise, // Auto-generated
381+
1 ( map ≡ Cons(p, next) ) by Premise, // auto-generated
382+
2 ( lookup(update(next, key1, value), key2) ≡ lookup(next, key2) ) by Premise, // auto-generated
373383
3 ( key1 ≢ key2 ) by Premise,
374384
4 ( !(p._1 ≡ key1) ) by Premise,
375385
5 ( !(p._1 ≡ key2) ) by Premise,
@@ -386,7 +396,7 @@ object List {
386396
case Nil() => {
387397
Deduce(
388398
//@formatter:off
389-
1 ( map ≡ Nil[(K, V)]() ) by Premise, // Auto-generated
399+
1 ( map ≡ Nil[(K, V)]() ) by Premise, // auto-generated
390400
2 ( key1 ≢ key2 ) by Premise,
391401
3 ( update(map, key1, value) ≡ Cons(key1 ~> value, Nil[(K, V)]()) ) by RSimpl(RS(update _)), //Auto,
392402
4 ( lookup(update(map, key1, value), key2) ≡ lookup(map, key2) ) by RSimpl(RS(lookup _)) //Auto,
@@ -615,7 +625,7 @@ object List {
615625
if (q.length < q.capacity) {
616626
Deduce(
617627
//@formatter:off
618-
1 ( q.strategy ≡ List.Queue.Strategy.DropEarliest ) by Premise, // Auto-generated
628+
1 ( q.strategy ≡ List.Queue.Strategy.DropEarliest ) by Premise, // auto-generated
619629
2 ( q.length < q.capacity ) by Premise,
620630
3 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
621631
4 ( q.push(a).strategy ≡ q.strategy ) by Simpl
@@ -625,7 +635,7 @@ object List {
625635
} else {
626636
Deduce(
627637
//@formatter:off
628-
1 ( q.strategy ≡ List.Queue.Strategy.DropEarliest ) by Premise, // Auto-generated
638+
1 ( q.strategy ≡ List.Queue.Strategy.DropEarliest ) by Premise, // auto-generated
629639
2 ( !(q.length < q.capacity) ) by Premise,
630640
3 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
631641
4 ( q.push(a).strategy ≡ q.strategy ) by Simpl
@@ -638,7 +648,7 @@ object List {
638648
if (q.length < q.capacity) {
639649
Deduce(
640650
//@formatter:off
641-
1 ( q.strategy ≡ List.Queue.Strategy.DropLatest ) by Premise, // Auto-generated
651+
1 ( q.strategy ≡ List.Queue.Strategy.DropLatest ) by Premise, // auto-generated
642652
2 ( q.length < q.capacity ) by Premise,
643653
3 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
644654
4 ( q.push(a).strategy ≡ q.strategy ) by Simpl
@@ -648,7 +658,7 @@ object List {
648658
} else {
649659
Deduce(
650660
//@formatter:off
651-
1 ( q.strategy ≡ List.Queue.Strategy.DropLatest ) by Premise, // Auto-generated
661+
1 ( q.strategy ≡ List.Queue.Strategy.DropLatest ) by Premise, // auto-generated
652662
2 ( !(q.length < q.capacity) ) by Premise,
653663
3 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
654664
4 ( q.push(a).strategy ≡ q.strategy ) by Simpl
@@ -661,7 +671,7 @@ object List {
661671
if (q.length < q.capacity) {
662672
Deduce(
663673
//@formatter:off
664-
1 ( q.strategy ≡ List.Queue.Strategy.Error ) by Premise, // Auto-generated
674+
1 ( q.strategy ≡ List.Queue.Strategy.Error ) by Premise, // auto-generated
665675
2 ( q.length < q.capacity ) by Premise,
666676
3 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
667677
4 ( q.push(a).strategy ≡ q.strategy ) by Simpl
@@ -671,7 +681,7 @@ object List {
671681
} else {
672682
Deduce(
673683
//@formatter:off
674-
1 ( q.strategy ≡ List.Queue.Strategy.Error ) by Premise, // Auto-generated
684+
1 ( q.strategy ≡ List.Queue.Strategy.Error ) by Premise, // auto-generated
675685
2 ( !(q.length < q.capacity) ) by Premise,
676686
3 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
677687
4 ( q.push(a).strategy ≡ q.strategy ) by Simpl
@@ -683,7 +693,7 @@ object List {
683693
case Queue.Strategy.Unbounded => {
684694
Deduce(
685695
//@formatter:off
686-
1 ( q.strategy ≡ List.Queue.Strategy.Unbounded ) by Premise, // Auto-generated
696+
1 ( q.strategy ≡ List.Queue.Strategy.Unbounded ) by Premise, // auto-generated
687697
2 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
688698
3 ( q.push(a).strategy ≡ q.strategy ) by Simpl
689699
//@formatter:on

‎shared/src/main/scala/org/sireum/logika/Logika.scala

+3-1
Original file line numberDiff line numberDiff line change
@@ -4569,7 +4569,7 @@ import Util._
45694569
else AST.Util.bigImply(T, cm.requires :+ AST.Util.bigAnd(cm.ensures, posOpt), posOpt)
45704570
var (s1, v) = evalExp(Split.Disabled, smt2, cache, rtCheck, state, stmt.exp, reporter)(0)
45714571
var branches = ISZ[Branch]()
4572-
lang.FrontEnd.induct(th, HashSet.empty, context.methodName, claim, stmt.exp, posOpt.get) match {
4572+
th.induct(T, HashSet.empty, context.methodName, claim, stmt.exp, posOpt.get) match {
45734573
case Some(ir) =>
45744574
val lcontext = context.methodName
45754575
var cases = ir.cases
@@ -5484,6 +5484,8 @@ import Util._
54845484
return (this, evalDeduceSteps(state, stmt))
54855485
case stmt: AST.Stmt.DeduceSequent if stmt.justOpt.isEmpty =>
54865486
return (this, evalDeduceSequent(state, stmt))
5487+
case stmt: AST.Stmt.Induct =>
5488+
return (this, for (sv <- evalExp(split, smt2, cache, rtCheck, state, stmt.exp, reporter)) yield sv._1)
54875489
case _: AST.Stmt.Object => return (this, ISZ(state))
54885490
case _: AST.Stmt.Import => return (this, ISZ(state))
54895491
case _: AST.Stmt.Method => return (this, ISZ(state))

0 commit comments

Comments
 (0)