diff --git a/jvm/src/test/scala/org/sireum/logika/example/list.sc b/jvm/src/test/scala/org/sireum/logika/example/list.sc index 8d809fdb..d31796b7 100644 --- a/jvm/src/test/scala/org/sireum/logika/example/list.sc +++ b/jvm/src/test/scala/org/sireum/logika/example/list.sc @@ -41,6 +41,15 @@ import org.sireum.justification._ this } + @strictpure def dropLax(n: Z): List[T] = if (n > 0) { + this match { + case List.Cons(_, next) => next.dropLax(n - 1) + case _ => List.empty + } + } else { + this + } + @strictpure def take(n: Z): List[T] = if (n > 0) { this match { case List.Cons(value, next) => List.Cons(value, next.take(n - 1)) @@ -49,6 +58,15 @@ import org.sireum.justification._ } else { List.empty } + + @strictpure def takeLax(n: Z): List[T] = if (n > 0) { + this match { + case List.Cons(value, next) => List.Cons(value, next.takeLax(n - 1)) + case _ => List.empty + } + } else { + List.empty + } } object List { @@ -57,6 +75,36 @@ object List { @datatype class Cons[T](val value: T, val next: List[T]) extends List[T] + @pure def emptyZeroLength[T](l: List[T]): Unit = { + Contract( + Ensures(l.length >= 0) + ) + + l match { + case Cons(a, next) => { + emptyZeroLength(next) + Deduce( + //@formatter:off + 1 ( l ≡ Cons(a, next) ) by Auto, + 2 ( next.length >= 0 ) by Premise, + 3 ( l.length ≡ (1 + next.length) ) by Simpl, + 4 ( l.length >= 0 ) by Auto and (2, 3) + //@formatter:on + ) + return + } + case _ => { + Deduce( + //@formatter:off + 1 ( l ≡ Nil[T]() ) by Auto, + 2 ( l.length >= 0 ) by Simpl + //@formatter:on + ) + return + } + } + } + type Map[K, V] = List[(K, V)] object Map { @@ -254,7 +302,7 @@ object List { @strictpure def drop(n: Z): Queue[T] = { val thiz = this - thiz(buffer = buffer.drop(n)) + thiz(buffer = buffer.dropLax(n)) } @strictpure def clear: Queue[T] = { @@ -294,6 +342,13 @@ object List { ) } + @pure def wfEmptyAuto[T](c: Z, s: Strategy.Type): Unit = { + Contract( + Requires(0 < c), + Ensures(empty[T](c, s).wellFormed) + ) + } + @pure def singleQueueHead[T](q: Queue[T], a: T): Unit = { Contract( Requires(q.buffer ≡ List.make(a)), @@ -301,12 +356,20 @@ object List { ) Deduce( //@formatter:off - 1 ( q.buffer ≡ List.make(a) ) by Premise, - 2 ( q.head ≡ a ) by Simpl // Auto + 1 ( q.buffer ≡ List.make(a) ) by Premise, + 2 ( q.buffer ≡ Cons[T](a, Nil()) ) by Eval(1), + 3 ( q.head ≡ a ) by Simpl // Auto //@formatter:on ) } + @pure def singleQueueHeadAuto[T](q: Queue[T], a: T): Unit = { + Contract( + Requires(q.buffer ≡ List.make(a)), + Ensures(q.head ≡ a) + ) + } + @pure def frameTail[T](q: Queue[T]): Unit = { Contract( Ensures( @@ -324,6 +387,16 @@ object List { ) } + @pure def frameTailAuto[T](q: Queue[T]): Unit = { + Contract( + Ensures( + q.tail.error ≡ q.error, + q.tail.capacity ≡ q.capacity, + q.tail.strategy ≡ q.strategy + ) + ) + } + @pure def wfTail[T](q: Queue[T]): Unit = { Contract( Requires(q.wellFormed), @@ -335,9 +408,9 @@ object List { Deduce( //@formatter:off 1 ( q.wellFormed ) by Premise, - 2 ( q.tail.error == q.error ) by Premise, - 3 ( q.tail.capacity == q.capacity ) by Premise, - 4 ( q.tail.strategy == q.strategy ) by Premise, + 2 ( q.tail.error ≡ q.error ) by Premise, + 3 ( q.tail.capacity ≡ q.capacity ) by Premise, + 4 ( q.tail.strategy ≡ q.strategy ) by Premise, 5 ( q.buffer.length >= q.tail.length ) by Auto, 6 ( 0 < q.capacity & (q.strategy != Queue.Strategy.Unbounded __>: q.buffer.length <= q.capacity) ) by Rewrite(RS(Queue.$.wellFormed _), 1), // Auto, @@ -348,6 +421,13 @@ object List { ) } + @pure def wfTailAuto[T](q: Queue[T]): Unit = { + Contract( + Requires(q.wellFormed), + Ensures(q.tail.wellFormed) + ) + } + @pure def singleQueueTail[T](q: Queue[T], a: T): Unit = { Contract( Requires(q.buffer ≡ List.make(a)), @@ -356,11 +436,20 @@ object List { Deduce( //@formatter:off 1 ( q.buffer ≡ List.make(a) ) by Premise, - 2 ( q.tail.buffer ≡ List.Nil[T]() ) by Simpl // Auto + 2 ( q.buffer ≡ Cons[T](a, Nil()) ) by Eval(1), + 3 ( q.tail.buffer ≡ List.Nil[T]() ) by Simpl, // Auto, + 4 ( q.tail.buffer ≡ List.empty[T] ) by Simpl // Auto //@formatter:on ) } + @pure def singleQueueTailAuto[T](q: Queue[T], a: T): Unit = { + Contract( + Requires(q.buffer ≡ List.make(a)), + Ensures(q.tail.buffer ≡ List.empty[T]) + ) + } + @pure def framePush[T](q: Queue[T], a: T): Unit = { Contract( Ensures( @@ -374,20 +463,20 @@ object List { if (q.length < q.capacity) { Deduce( //@formatter:off - 1 ( q.strategy == List.Queue.Strategy.DropEarliest ) by Auto, - 2 ( q.length < q.capacity ) by Premise, - 3 ( q.push(a).capacity ≡ q.capacity ) by Simpl, - 4 ( q.push(a).strategy ≡ q.strategy ) by Simpl + 1 ( q.strategy ≡ List.Queue.Strategy.DropEarliest ) by Premise, + 2 ( q.length < q.capacity ) by Premise, + 3 ( q.push(a).capacity ≡ q.capacity ) by Simpl, + 4 ( q.push(a).strategy ≡ q.strategy ) by Simpl //@formatter:on ) return } else { Deduce( //@formatter:off - 1 ( q.strategy == List.Queue.Strategy.DropEarliest ) by Auto, - 2 ( !(q.length < q.capacity) ) by Premise, - 3 ( q.push(a).capacity ≡ q.capacity ) by Simpl, - 4 ( q.push(a).strategy ≡ q.strategy ) by Simpl + 1 ( q.strategy ≡ List.Queue.Strategy.DropEarliest ) by Premise, + 2 ( !(q.length < q.capacity) ) by Premise, + 3 ( q.push(a).capacity ≡ q.capacity ) by Simpl, + 4 ( q.push(a).strategy ≡ q.strategy ) by Simpl //@formatter:on ) return @@ -397,20 +486,20 @@ object List { if (q.length < q.capacity) { Deduce( //@formatter:off - 1 ( q.strategy == List.Queue.Strategy.DropLatest ) by Auto, - 2 ( q.length < q.capacity ) by Premise, - 3 ( q.push(a).capacity ≡ q.capacity ) by Simpl, - 4 ( q.push(a).strategy ≡ q.strategy ) by Simpl + 1 ( q.strategy ≡ List.Queue.Strategy.DropLatest ) by Premise, + 2 ( q.length < q.capacity ) by Premise, + 3 ( q.push(a).capacity ≡ q.capacity ) by Simpl, + 4 ( q.push(a).strategy ≡ q.strategy ) by Simpl //@formatter:on ) return } else { Deduce( //@formatter:off - 1 ( q.strategy == List.Queue.Strategy.DropLatest ) by Auto, - 2 ( !(q.length < q.capacity) ) by Premise, - 3 ( q.push(a).capacity ≡ q.capacity ) by Simpl, - 4 ( q.push(a).strategy ≡ q.strategy ) by Simpl + 1 ( q.strategy ≡ List.Queue.Strategy.DropLatest ) by Premise, + 2 ( !(q.length < q.capacity) ) by Premise, + 3 ( q.push(a).capacity ≡ q.capacity ) by Simpl, + 4 ( q.push(a).strategy ≡ q.strategy ) by Simpl //@formatter:on ) return @@ -420,20 +509,20 @@ object List { if (q.length < q.capacity) { Deduce( //@formatter:off - 1 ( q.strategy == List.Queue.Strategy.Error ) by Auto, - 2 ( q.length < q.capacity ) by Premise, - 3 ( q.push(a).capacity ≡ q.capacity ) by Simpl, - 4 ( q.push(a).strategy ≡ q.strategy ) by Simpl + 1 ( q.strategy ≡ List.Queue.Strategy.Error ) by Premise, + 2 ( q.length < q.capacity ) by Premise, + 3 ( q.push(a).capacity ≡ q.capacity ) by Simpl, + 4 ( q.push(a).strategy ≡ q.strategy ) by Simpl //@formatter:on ) return } else { Deduce( //@formatter:off - 1 ( q.strategy == List.Queue.Strategy.Error ) by Auto, - 2 ( !(q.length < q.capacity) ) by Premise, - 3 ( q.push(a).capacity ≡ q.capacity ) by Simpl, - 4 ( q.push(a).strategy ≡ q.strategy ) by Simpl + 1 ( q.strategy ≡ List.Queue.Strategy.Error ) by Premise, + 2 ( !(q.length < q.capacity) ) by Premise, + 3 ( q.push(a).capacity ≡ q.capacity ) by Simpl, + 4 ( q.push(a).strategy ≡ q.strategy ) by Simpl //@formatter:on ) return @@ -442,9 +531,9 @@ object List { case Queue.Strategy.Unbounded => { Deduce( //@formatter:off - 1 ( q.strategy == List.Queue.Strategy.Unbounded ) by Auto, - 2 ( q.push(a).capacity ≡ q.capacity ) by Simpl, - 3 ( q.push(a).strategy ≡ q.strategy ) by Simpl + 1 ( q.strategy ≡ List.Queue.Strategy.Unbounded ) by Premise, + 2 ( q.push(a).capacity ≡ q.capacity ) by Simpl, + 3 ( q.push(a).strategy ≡ q.strategy ) by Simpl //@formatter:on ) return @@ -462,9 +551,9 @@ object List { case Queue.Strategy.DropEarliest => { Deduce( //@formatter:off - 1 ( q.length < q.capacity ) by Premise, - 2 ( q.strategy == List.Queue.Strategy.DropEarliest ) by Auto, - 3 ( q.push(a).buffer ≡ (q.buffer ++ List.make(a)) ) by Simpl + 1 ( q.length < q.capacity ) by Premise, + 2 ( q.strategy ≡ List.Queue.Strategy.DropEarliest ) by Premise, + 3 ( q.push(a).buffer ≡ (q.buffer ++ List.make(a)) ) by Simpl //@formatter:on ) return @@ -473,7 +562,7 @@ object List { Deduce( //@formatter:off 1 ( q.length < q.capacity ) by Premise, - 2 ( q.strategy == List.Queue.Strategy.DropLatest ) by Auto, + 2 ( q.strategy ≡ List.Queue.Strategy.DropLatest ) by Premise, 3 ( q.push(a).buffer ≡ (q.buffer ++ List.make(a)) ) by Simpl //@formatter:on ) @@ -483,7 +572,7 @@ object List { Deduce( //@formatter:off 1 ( q.length < q.capacity ) by Premise, - 2 ( q.strategy == List.Queue.Strategy.Error ) by Auto, + 2 ( q.strategy ≡ List.Queue.Strategy.Error ) by Premise, 3 ( q.push(a).buffer ≡ (q.buffer ++ List.make(a)) ) by Simpl //@formatter:on ) @@ -492,7 +581,7 @@ object List { case Queue.Strategy.Unbounded => { Deduce( //@formatter:off - 1 ( q.strategy == List.Queue.Strategy.Unbounded ) by Auto, + 1 ( q.strategy ≡ List.Queue.Strategy.Unbounded ) by Premise, 2 ( q.push(a).capacity ≡ q.capacity ) by Simpl, 3 ( q.push(a).buffer ≡ (q.buffer ++ List.make(a)) ) by Simpl //@formatter:on @@ -507,6 +596,7 @@ object List { Requires(q.wellFormed), Ensures(q.push(a).wellFormed) ) + setOptions("Logika", """--rw-eval-trace --par --par-branch --background disabled""") framePush(q, a) @@ -518,13 +608,13 @@ object List { Deduce( //@formatter:off - 1 ( q.wellFormed ) by Premise, - 2 ( q.push(a).capacity == q.capacity ) by Premise, - 3 ( q.push(a).strategy == q.strategy ) by Premise, - 4 ( q.strategy == List.Queue.Strategy.DropEarliest ) by Auto, - 5 ( q.length < q.capacity ) by Premise, - 6 ( q.push(a).buffer ≡ (q.buffer ++ List.make(a)) ) by Auto, - 7 ( q.push(a).wellFormed ) by Simpl + 1 ( q.wellFormed ) by Premise, + 2 ( q.push(a).capacity ≡ q.capacity ) by Premise, + 3 ( q.push(a).strategy ≡ q.strategy ) by Premise, + 4 ( q.strategy ≡ List.Queue.Strategy.DropEarliest ) by Premise, + 5 ( q.length < q.capacity ) by Premise, + 6 ( q.push(a).buffer ≡ (q.buffer ++ List.make(a)) ) by Simpl, // Auto + 7 ( q.push(a).wellFormed ) by Simpl //@formatter:on ) return @@ -532,9 +622,9 @@ object List { Deduce( //@formatter:off 1 ( q.wellFormed ) by Premise, - 2 ( q.push(a).capacity == q.capacity ) by Premise, - 3 ( q.push(a).strategy == q.strategy ) by Premise, - 4 ( q.strategy == List.Queue.Strategy.DropEarliest ) by Auto, + 2 ( q.push(a).capacity ≡ q.capacity ) by Premise, + 3 ( q.push(a).strategy ≡ q.strategy ) by Premise, + 4 ( q.strategy ≡ List.Queue.Strategy.DropEarliest ) by Premise, 5 ( !(q.length < q.capacity) ) by Premise, 6 ( q.push(a).buffer ≡ (q.buffer.tlLax ++ List.make(a)) ) by Simpl, 7 ( q.push(a).wellFormed ) by Simpl @@ -551,9 +641,9 @@ object List { Deduce( //@formatter:off 1 ( q.wellFormed ) by Premise, - 2 ( q.push(a).capacity == q.capacity ) by Premise, - 3 ( q.push(a).strategy == q.strategy ) by Premise, - 4 ( q.strategy == List.Queue.Strategy.DropLatest ) by Auto, + 2 ( q.push(a).capacity ≡ q.capacity ) by Premise, + 3 ( q.push(a).strategy ≡ q.strategy ) by Premise, + 4 ( q.strategy ≡ List.Queue.Strategy.DropLatest ) by Premise, 5 ( q.length < q.capacity ) by Premise, 6 ( q.push(a).buffer ≡ (q.buffer ++ List.make(a)) ) by Simpl, // Auto, 7 ( q.push(a).wellFormed ) by Simpl @@ -563,13 +653,13 @@ object List { } else { Deduce( //@formatter:off - 1 ( q.wellFormed ) by Premise, - 2 ( q.push(a).capacity == q.capacity ) by Premise, - 3 ( q.push(a).strategy == q.strategy ) by Premise, - 4 ( q.strategy == List.Queue.Strategy.DropLatest ) by Auto, - 5 ( !(q.length < q.capacity) ) by Premise, - 6 ( q.push(a).buffer ≡ q.buffer ) by Simpl, // Auto, - 7 ( q.push(a).wellFormed ) by Simpl // Auto + 1 ( q.wellFormed ) by Premise, + 2 ( q.push(a).capacity ≡ q.capacity ) by Premise, + 3 ( q.push(a).strategy ≡ q.strategy ) by Premise, + 4 ( q.strategy ≡ List.Queue.Strategy.DropLatest ) by Premise, + 5 ( !(q.length < q.capacity) ) by Premise, + 6 ( q.push(a).buffer ≡ q.buffer ) by Simpl, // Auto, + 7 ( q.push(a).wellFormed ) by Simpl // Auto //@formatter:on ) return @@ -583,9 +673,9 @@ object List { Deduce( //@formatter:off 1 ( q.wellFormed ) by Premise, - 2 ( q.push(a).capacity == q.capacity ) by Premise, - 3 ( q.push(a).strategy == q.strategy ) by Premise, - 4 ( q.strategy == List.Queue.Strategy.Error ) by Auto, + 2 ( q.push(a).capacity ≡ q.capacity ) by Premise, + 3 ( q.push(a).strategy ≡ q.strategy ) by Premise, + 4 ( q.strategy ≡ List.Queue.Strategy.Error ) by Premise, 5 ( q.length < q.capacity ) by Premise, 6 ( q.push(a).buffer ≡ (q.buffer ++ List.make(a)) ) by Simpl, // Auto, 7 ( q.push(a).wellFormed ) by Simpl @@ -595,13 +685,13 @@ object List { } else { Deduce( //@formatter:off - 1 ( q.wellFormed ) by Premise, - 2 ( q.push(a).capacity == q.capacity ) by Premise, - 3 ( q.push(a).strategy == q.strategy ) by Premise, - 4 ( q.strategy == List.Queue.Strategy.Error ) by Auto, - 5 ( !(q.length < q.capacity) ) by Premise, - 6 ( q.push(a).buffer ≡ List.empty[T] ) by Simpl, // Auto, - 7 ( q.push(a).wellFormed ) by Simpl // Auto + 1 ( q.wellFormed ) by Premise, + 2 ( q.push(a).capacity ≡ q.capacity ) by Premise, + 3 ( q.push(a).strategy ≡ q.strategy ) by Premise, + 4 ( q.strategy ≡ List.Queue.Strategy.Error ) by Premise, + 5 ( !(q.length < q.capacity) ) by Premise, + 6 ( q.push(a).buffer ≡ List.empty[T] ) by Simpl, // Auto, + 7 ( q.push(a).wellFormed ) by Simpl // Auto //@formatter:on ) return @@ -611,9 +701,9 @@ object List { Deduce( //@formatter:off 1 ( q.wellFormed ) by Premise, - 2 ( q.push(a).capacity == q.capacity ) by Premise, - 3 ( q.push(a).strategy == q.strategy ) by Premise, - 4 ( q.strategy == List.Queue.Strategy.Unbounded ) by Auto, + 2 ( q.push(a).capacity ≡ q.capacity ) by Premise, + 3 ( q.push(a).strategy ≡ q.strategy ) by Premise, + 4 ( q.strategy ≡ List.Queue.Strategy.Unbounded ) by Premise, 5 ( q.push(a).buffer ≡ (q.buffer ++ List.make(a)) ) by Simpl, 6 ( q.push(a).wellFormed ) by Simpl //@formatter:on @@ -623,6 +713,225 @@ object List { } } + + @pure def frameDrop[T](q: Queue[T], n: Z): Unit = { + Contract( + Ensures( + q.drop(n).capacity ≡ q.capacity, + q.drop(n).strategy ≡ q.strategy, + q.drop(n).error ≡ q.error + ) + ) + + Deduce( + //@formatter:off + 1 ( q.drop(n).capacity ≡ q.capacity ) by Simpl, + 2 ( q.drop(n).strategy ≡ q.strategy ) by Simpl, + 3 ( q.drop(n).error ≡ q.error ) by Simpl + //@formatter:on + ) + } + + @pure def dropLeLength[T](l: List[T], n: Z): Unit = { + Contract( + Ensures(l.length >= l.dropLax(n).length) + ) + + if (n > 0) { + l match { + case Cons(e, next) => { + dropLeLength(next, n - 1) + + Deduce( + //@formatter:off + 1 ( n > 0 ) by Premise, + 2 ( l ≡ Cons(e, next) ) by Auto, + 3 ( next.length >= next.dropLax(n - 1).length ) by Premise, + 4 ( l.dropLax(n).length ≡ next.dropLax(n - 1).length ) by Simpl, + 5 ( next.length >= l.dropLax(n).length ) by Subst_>(4, 3), + 6 ( l.length ≡ (1 + next.length) ) by Simpl, + 7 ( l.length >= l.dropLax(n).length ) by Auto and (5, 6) + //@formatter:on + ) + return + } + case _ => { + Deduce( + //@formatter:off + 1 ( n > 0 ) by Premise, + 2 ( l ≡ Nil[T]() ) by Auto, + 3 ( l.dropLax(n) ≡ Nil[T]() ) by Simpl, + 4 ( l.length >= l.dropLax(n).length ) by Simpl + //@formatter:on + ) + return + } + } + } else { + Deduce( + //@formatter:off + 1 ( !(n > 0) ) by Premise, + 2 ( l ≡ l.dropLax(n) ) by Simpl, + 3 ( l.length >= l.dropLax(n).length ) by Simpl + //@formatter:on + ) + return + } + + } + + @pure def wfDrop[T](q: Queue[T], n: Z): Unit = { + Contract( + Requires(q.wellFormed), + Ensures(q.drop(n).wellFormed) + ) + + frameDrop(q, n) + dropLeLength(q.buffer, n) + + Deduce( + //@formatter:off + 1 ( q.wellFormed ) by Premise, + 2 ( q.drop(n).capacity ≡ q.capacity ) by Premise, + 3 ( q.drop(n).strategy ≡ q.strategy ) by Premise, + 4 ( q.drop(n).error ≡ q.error ) by Premise, + 5 ( q.buffer.length >= q.buffer.dropLax(n).length ) by Premise, + 6 ( q.buffer.dropLax(n).length ≡ q.drop(n).length ) by Simpl, + 7 ( q.buffer.length >= q.drop(n).length ) by Subst_<(6, 5), + 8 ( 0 < q.capacity & + (q.strategy != Queue.Strategy.Unbounded __>: q.buffer.length <= q.capacity) ) by Rewrite(RS(Queue.$.wellFormed _), 1), // Auto, + 9 ( 0 < q.drop(n).capacity & + (q.drop(n).strategy != Queue.Strategy.Unbounded __>: q.drop(n).length <= q.drop(n).capacity) ) by Auto, + 10 ( q.drop(n).wellFormed ) by Rewrite(RS(Queue.$.wellFormed _), 9) + //@formatter:on + ) + } + + @pure def frameClear[T](q: Queue[T]): Unit = { + Contract( + Ensures( + q.clear.capacity ≡ q.capacity, + q.clear.strategy ≡ q.strategy, + q.clear.error ≡ q.error + ) + ) + Deduce( + //@formatter:off + 1 ( q.clear.capacity ≡ q.capacity ) by Simpl, + 2 ( q.clear.strategy ≡ q.strategy ) by Simpl, + 3 ( q.clear.error ≡ q.error ) by Simpl + //@formatter:on + ) + } + + @pure def frameClearAuto[T](q: Queue[T]): Unit = { + Contract( + Ensures( + q.clear.capacity ≡ q.capacity, + q.clear.strategy ≡ q.strategy, + q.clear.error ≡ q.error + ) + ) + } + + @pure def wfClear[T](q: Queue[T]): Unit = { + Contract( + Requires(q.wellFormed), + Ensures(q.clear.wellFormed) + ) + emptyZeroLength(q.buffer) + frameClear(q) + Deduce( + //@formatter:off + 1 ( q.wellFormed ) by Premise, + 2 ( q.clear.capacity ≡ q.capacity ) by Premise, + 3 ( q.clear.strategy ≡ q.strategy ) by Premise, + 4 ( q.clear.error ≡ q.error ) by Premise, + 5 ( q.clear.buffer.length ≡ 0 ) by Simpl, + 6 ( 0 < q.capacity & + (q.strategy != Queue.Strategy.Unbounded __>: q.buffer.length <= q.capacity) ) by Rewrite(RS(Queue.$.wellFormed _), 1), // Auto, + 7 ( 0 < q.capacity ) by Simpl, + 8 ( 0 < q.clear.capacity & + (q.clear.strategy != Queue.Strategy.Unbounded __>: q.buffer.length <= q.clear.capacity) ) by Auto, + 9 ( 0 < q.clear.capacity & + (q.clear.strategy != Queue.Strategy.Unbounded __>: q.clear.buffer.length <= q.clear.capacity) ) by Simpl, + 10 ( q.clear.wellFormed ) by RSimpl(RS(Queue.$.wellFormed _)) + //@formatter:on + ) + } + + @pure def wfClearAuto[T](q: Queue[T]): Unit = { + Contract( + Requires(q.wellFormed), + Ensures(q.clear.wellFormed) + ) + } + + @pure def frameSetBuffer[T](q: Queue[T], l: List[T]): Unit = { + Contract( + Ensures( + q.setBuffer(l).capacity ≡ q.capacity, + q.setBuffer(l).strategy ≡ q.strategy, + q.setBuffer(l).error ≡ q.error + ) + ) + Deduce( + //@formatter:off + 1 ( q.setBuffer(l).capacity ≡ q.capacity ) by Simpl, + 2 ( q.setBuffer(l).strategy ≡ q.strategy ) by Simpl, + 3 ( q.setBuffer(l).error ≡ q.error ) by Simpl + //@formatter:on + ) + } + + @pure def frameSetBufferAuto[T](q: Queue[T], l: List[T]): Unit = { + Contract( + Ensures( + q.setBuffer(l).capacity ≡ q.capacity, + q.setBuffer(l).strategy ≡ q.strategy, + q.setBuffer(l).error ≡ q.error + ) + ) + } + + @pure def wfSetBuffer[T](q: Queue[T], l: List[T]): Unit = { + Contract( + Requires( + q.wellFormed, + l.length <= q.capacity + ), + Ensures(q.setBuffer(l).wellFormed) + ) + frameSetBuffer(q, l) + Deduce( + //@formatter:off + 1 ( q.wellFormed ) by Premise, + 2 ( l.length <= q.capacity ) by Premise, + 3 ( q.setBuffer(l).capacity ≡ q.capacity ) by Premise, + 4 ( q.setBuffer(l).strategy ≡ q.strategy ) by Premise, + 5 ( q.setBuffer(l).error ≡ q.error ) by Premise, + 6 ( q.setBuffer(l).length ≡ l.length ) by Simpl, + 7 ( q.setBuffer(l).length <= q.capacity ) by Subst_>(6, 2), + 8 ( q.setBuffer(l).length <= q.setBuffer(l).capacity ) by Subst_>(3, 7), + 9 ( 0 < q.capacity & + (q.strategy != Queue.Strategy.Unbounded __>: q.buffer.length <= q.capacity) ) by Rewrite(RS(Queue.$.wellFormed _), 1), // Auto, + 10 ( 0 < q.setBuffer(l).capacity & + (q.setBuffer(l).strategy != Queue.Strategy.Unbounded __>: q.setBuffer(l).buffer.length <= q.setBuffer(l).capacity) ) by Auto, + 11 ( q.setBuffer(l).wellFormed ) by Rewrite(RS(Queue.$.wellFormed _), 10) + //@formatter:on + ) + + } + + @pure def wfSetBufferAuto[T](q: Queue[T], l: List[T]): Unit = { + Contract( + Requires( + q.wellFormed, + l.length <= q.capacity + ), + Ensures(q.setBuffer(l).wellFormed) + ) + } } diff --git a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala index 6627fb44..2bf47d7d 100644 --- a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala +++ b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala @@ -1716,6 +1716,9 @@ object RewritingSystem { for (i <- 0 until params.size) { map = map + (params.size - i) ~> args(i) } + if (f.param.tipe == AST.Typed.unit && args.isEmpty) { + return Some((f.exp, 0)) + } ParamSubstitutor(map).transformCoreExpBase(body) match { case MSome(body2) => if (args.size > params.size) { @@ -1794,7 +1797,7 @@ object RewritingSystem { val f = pattern.toFun receiverOpt match { case Some(receiver) => return AST.CoreExp.Apply(f, ISZ(receiver), f.exp.tipe) - case _ => return f + case _ => return if (info.ast.sig.funType.isByName) AST.CoreExp.Apply(f, ISZ(), f.exp.tipe) else f } } @@ -1809,8 +1812,6 @@ object RewritingSystem { case (_, right: AST.CoreExp.Lit) => r = r + left ~> (right, stepId) case (left: AST.CoreExp.Constructor, _) => r = r + right ~> (left, stepId) case (_, right: AST.CoreExp.Constructor) => r = r + left ~> (right, stepId) - case (left: AST.CoreExp.Apply, _) => r = r + right ~> (left, stepId) - case (_, right: AST.CoreExp.Apply) => r = r + left ~> (right, stepId) case (_, _) => val (key, value): (AST.CoreExp.Base, AST.CoreExp.Base) = if (left < right) (right, left) else (left, right) @@ -1833,6 +1834,7 @@ object RewritingSystem { var trace = ISZ[Trace]() def evalBaseH(e: AST.CoreExp.Base): Option[AST.CoreExp.Base] = { + var rOpt = Option.none[AST.CoreExp.Base]() if (e.tipe == AST.Typed.b) { provenClaims.get(e) match { case Some(stepId) => @@ -1840,49 +1842,53 @@ object RewritingSystem { if (shouldTrace) { trace = trace :+ Trace.Eval(st"using $stepId", e, r) } - return Some(r) + rOpt = Some(r) case _ => } - provenClaims.get(AST.CoreExp.Unary(AST.Exp.UnaryOp.Not, e)) match { - case Some(stepId) => - val r = AST.CoreExp.False - if (shouldTrace) { - trace = trace :+ Trace.Eval(st"using $stepId", e, r) - } - return Some(r) - case _ => + if (rOpt.isEmpty) { + provenClaims.get(AST.CoreExp.Unary(AST.Exp.UnaryOp.Not, e)) match { + case Some(stepId) => + val r = AST.CoreExp.False + if (shouldTrace) { + trace = trace :+ Trace.Eval(st"using $stepId", e, r) + } + rOpt = Some(r) + case _ => + } } } - if (config.equivSubst) { + if (rOpt.isEmpty && config.equivSubst) { val r = eqMap.get(e) r match { case Some((to, stepId)) => if (shouldTrace) { trace = trace :+ Trace.Eval(st"substitution using $stepId [${to.prettyST}/${e.prettyST}]", e, to) } - return Some(to) + rOpt = Some(to) case _ => } } - var rOpt: Option[AST.CoreExp.Base] = e match { - case _: AST.CoreExp.Halt => None() - case _: AST.CoreExp.Lit => None() - case _: AST.CoreExp.LocalVarRef => None() - case e: AST.CoreExp.ParamVarRef => evalParamVarRef(e) - case e: AST.CoreExp.VarRef => evalVarRef(e) - case e: AST.CoreExp.Binary => evalBinary(e) - case e: AST.CoreExp.Unary => evalUnary(e) - case e: AST.CoreExp.Select => evalSelect(e) - case e: AST.CoreExp.Update => evalUpdate(e) - case e: AST.CoreExp.Indexing => evalIndexing(e) - case e: AST.CoreExp.IndexingUpdate => evalIndexingUpdate(e) - case e: AST.CoreExp.Constructor => evalConstructor(e) - case e: AST.CoreExp.If => evalIf(e) - case e: AST.CoreExp.Apply => evalApply(e) - case e: AST.CoreExp.Fun => evalFun(e) - case e: AST.CoreExp.Quant => evalQuant(e) - case e: AST.CoreExp.InstanceOfExp => evalInstanceOf(e) - case e: AST.CoreExp.Labeled => evalLabeled(e) + if (rOpt.isEmpty) { + rOpt = e match { + case _: AST.CoreExp.Halt => None() + case _: AST.CoreExp.Lit => None() + case _: AST.CoreExp.LocalVarRef => None() + case e: AST.CoreExp.ParamVarRef => evalParamVarRef(e) + case e: AST.CoreExp.VarRef => evalVarRef(e) + case e: AST.CoreExp.Binary => evalBinary(e) + case e: AST.CoreExp.Unary => evalUnary(e) + case e: AST.CoreExp.Select => evalSelect(e) + case e: AST.CoreExp.Update => evalUpdate(e) + case e: AST.CoreExp.Indexing => evalIndexing(e) + case e: AST.CoreExp.IndexingUpdate => evalIndexingUpdate(e) + case e: AST.CoreExp.Constructor => evalConstructor(e) + case e: AST.CoreExp.If => evalIf(e) + case e: AST.CoreExp.Apply => evalApply(e) + case e: AST.CoreExp.Fun => evalFun(e) + case e: AST.CoreExp.Quant => evalQuant(e) + case e: AST.CoreExp.InstanceOfExp => evalInstanceOf(e) + case e: AST.CoreExp.Labeled => evalLabeled(e) + } } rOpt match { case Some(r) => @@ -2065,19 +2071,7 @@ object RewritingSystem { case _ => } if (config.equality) { - var eq = F - var stepIdOpt = Option.none[ST]() if (left == right) { - eq = T - } else { - provenClaims.get(equiv(left, right)) match { - case Some(stepId) => - stepIdOpt = Some(st" ($stepId)") - eq = T - case _ => - } - } - if (eq) { rOpt = e.op match { case AST.Exp.BinaryOp.EquivUni => Some(AST.CoreExp.True) case AST.Exp.BinaryOp.InequivUni => Some(AST.CoreExp.False) @@ -2092,7 +2086,7 @@ object RewritingSystem { rOpt match { case Some(r) => if (shouldTrace) { - trace = trace :+ Trace.Eval(st"equivalence$stepIdOpt ${equivST(left, right)}", e, r) + trace = trace :+ Trace.Eval(st"equivalence ${equivST(left, right)}", e, r) } return rOpt case _ => @@ -2103,8 +2097,6 @@ object RewritingSystem { rOpt = e.op match { case AST.Exp.BinaryOp.EquivUni => Some(AST.CoreExp.False) case AST.Exp.BinaryOp.InequivUni => Some(AST.CoreExp.True) - case AST.Exp.BinaryOp.Eq => Some(AST.CoreExp.False) - case AST.Exp.BinaryOp.Ne => Some(AST.CoreExp.True) case _ => None() } rOpt match { diff --git a/shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala index 28ca0b4f..00edef98 100644 --- a/shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala +++ b/shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala @@ -30,6 +30,7 @@ import org.sireum.lang.{ast => AST} import org.sireum.lang.tipe.TypeHierarchy import org.sireum.logika.{Config, Logika, Smt2, Smt2Query, State, StepProofContext} import org.sireum.logika.Logika.Reporter +import org.sireum.logika.plugin.AutoPlugin.conjuncts object AutoPlugin { @record class MAlgebraChecker(var reporter: Reporter) extends AST.MTransformer { @@ -142,7 +143,40 @@ object AutoPlugin { } } - def detectOrIntro(th: TypeHierarchy, claim: AST.Exp, pc: ISZ[AST.Exp]): Option[ST] = { + @strictpure def conjuncts(e: AST.Exp): ISZ[AST.Exp] = { + e match { + case e: AST.Exp.Binary if e.attr.resOpt.get == AST.ResolvedInfo.BuiltIn(AST.ResolvedInfo.BuiltIn.Kind.BinaryAnd) => + conjuncts(e.left) ++ conjuncts(e.right) + case _ => ISZ(e) + } + } + + def detectOrIntro(th: TypeHierarchy, claimNorm: AST.Exp, claim: AST.Exp, conjuncts: ISZ[AST.Exp], pc: ISZ[AST.Exp]): Option[ST] = { + @strictpure def inPc: Some[ST] = Some( + st"""Accepted because ${claim.prettyST} is in the path conditions: + |{ + | ${(for (e <- pc) yield e.prettyST, ",\n")} + |}""" + ) + claimNorm match { + case claimNorm: AST.Exp.Binary => + claimNorm.attr.resOpt match { + case Some(res: AST.ResolvedInfo.BuiltIn) => + res.kind match { + case AST.ResolvedInfo.BuiltIn.Kind.BinaryEquiv if th.isSubstitutableWithoutSpecVars(claimNorm.left.typedOpt.get) => + if ((HashSet ++ conjuncts).contains(claimNorm(op = AST.Exp.BinaryOp.Eq, attr = claimNorm.attr(resOpt = Some(res(kind = AST.ResolvedInfo.BuiltIn.Kind.BinaryEq)))))) { + return inPc + } + case AST.ResolvedInfo.BuiltIn.Kind.BinaryInequiv if th.isSubstitutableWithoutSpecVars(claimNorm.left.typedOpt.get) => + if ((HashSet ++ conjuncts).contains(claimNorm(op = AST.Exp.BinaryOp.Ne, attr = claimNorm.attr(resOpt = Some(res(kind = AST.ResolvedInfo.BuiltIn.Kind.BinaryNe)))))) { + return inPc + } + case _ => + } + case _ => + } + case _ => + } val (left, right): (AST.Exp, AST.Exp) = claim match { case claim: AST.Exp.Binary => claim.attr.resOpt match { @@ -159,7 +193,7 @@ object AutoPlugin { var posAntecedents = HashMap.empty[(AST.Exp, AST.Exp), AST.Exp.Binary] var negAntecedents = HashMap.empty[(AST.Exp, AST.Exp), AST.Exp.Binary] - for (c <- pc) { + for (c <- conjuncts) { c match { case c: AST.Exp.Binary => c.attr.resOpt match { @@ -331,20 +365,22 @@ object AutoPlugin { } return logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter) } else if (id == "Premise") { - AutoPlugin.detectOrIntro(logika.th, step.claim, pathConditions) match { - case Some(acceptMsg) => - if (logika.config.detailedInfo) { - reporter.inform(pos, Logika.Reporter.Info.Kind.Verified, acceptMsg.render) - } - return logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter) - case _ => - reporter.error(posOpt, Logika.kind, - st"""The stated claim has not been proven before nor is a premise in the path conditions: - |{ - | ${(for (e <- pathConditions) yield e.prettyST, ";\n")} - |}""".render) - return err + for (pc <- normPathConditions.elements) { + AutoPlugin.detectOrIntro(logika.th, claimNorm, step.claim, conjuncts(pc), pathConditions) match { + case Some(acceptMsg) => + if (logika.config.detailedInfo) { + reporter.inform(pos, Logika.Reporter.Info.Kind.Verified, acceptMsg.render) + } + return logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter) + case _ => + } } + reporter.error(posOpt, Logika.kind, + st"""The stated claim has not been proven before nor is a premise in the path conditions: + |{ + | ${(for (e <- pathConditions) yield e.prettyST, ";\n")} + |}""".render) + return err } case _ => if (id == "Premise") {