Skip to content

Commit

Permalink
Rewriting system.
Browse files Browse the repository at this point in the history
  • Loading branch information
@robby-phd
robby-phd committed Mar 16, 2024
1 parent 814520e commit fa1b543
Show file tree
Hide file tree
Showing 5 changed files with 266 additions and 73 deletions.
166 changes: 160 additions & 6 deletions jvm/src/test/scala/org/sireum/logika/example/list.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -296,13 +296,13 @@ object List {

@pure def singleQueueHead[T](q: Queue[T], a: T): Unit = {
Contract(
Requires(q.buffer ≡ Cons[T](a, Nil())),
Requires(q.buffer ≡ List.make(a)),
Ensures(q.head ≡ a)
)
Deduce(
//@formatter:off
1 ( q.buffer ≡ List.Cons[T](a, List.Nil[T]()) ) by Premise,
2 ( q.head ≡ a ) by Simpl // Auto
1 ( q.buffer ≡ List.make(a) ) by Premise,
2 ( q.head ≡ a ) by Simpl // Auto
//@formatter:on
)
}
Expand All @@ -317,9 +317,9 @@ object List {
)
Deduce(
//@formatter:off
1 ( q.tail.error ≡ q.error ) by Simpl,
2 ( q.tail.capacity ≡ q.capacity ) by Simpl,
3 ( q.tail.strategy ≡ q.strategy ) by Simpl
1 ( q.tail.error ≡ q.error ) by Simpl, // Auto,
2 ( q.tail.capacity ≡ q.capacity ) by Simpl, // Auto,
3 ( q.tail.strategy ≡ q.strategy ) by Simpl // Auto
//@formatter:on
)
}
Expand Down Expand Up @@ -347,6 +347,160 @@ object List {
//@formatter:on
)
}

@pure def singleQueueTail[T](q: Queue[T], a: T): Unit = {
Contract(
Requires(q.buffer ≡ List.make(a)),
Ensures(q.tail.buffer ≡ List.empty[T])
)
Deduce(
//@formatter:off
1 ( q.buffer ≡ List.make(a) ) by Premise,
2 ( q.tail.buffer ≡ List.Nil[T]() ) by Simpl // Auto
//@formatter:on
)
}

@pure def framePush[T](q: Queue[T], a: T): Unit = {
Contract(
Ensures(
q.push(a).capacity ≡ q.capacity,
q.push(a).strategy ≡ q.strategy
)
)

q.strategy match {
case Queue.Strategy.DropEarliest => {
if (q.length < q.capacity) {
Deduce(
//@formatter:off
1 ( q.length < q.capacity ) by Premise,
2 ( q.strategy == List.Queue.Strategy.DropEarliest ) by Auto,
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.length < q.capacity) ) by Premise,
2 ( q.strategy == List.Queue.Strategy.DropEarliest ) by Auto,
3 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
4 ( q.push(a).strategy ≡ q.strategy ) by Simpl
//@formatter:on
)
return
}
}
case Queue.Strategy.DropLatest => {
if (q.length < q.capacity) {
Deduce(
//@formatter:off
1 ( q.length < q.capacity ) by Premise,
2 ( q.strategy == List.Queue.Strategy.DropLatest ) by Auto,
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.length < q.capacity) ) by Premise,
2 ( q.strategy == List.Queue.Strategy.DropLatest ) by Auto,
3 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
4 ( q.push(a).strategy ≡ q.strategy ) by Simpl
//@formatter:on
)
return
}
}
case Queue.Strategy.Error => {
if (q.length < q.capacity) {
Deduce(
//@formatter:off
1 ( q.length < q.capacity ) by Premise,
2 ( q.strategy == List.Queue.Strategy.Error ) by Auto,
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.length < q.capacity) ) by Premise,
2 ( q.strategy == List.Queue.Strategy.Error ) by Auto,
3 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
4 ( q.push(a).strategy ≡ q.strategy ) by Simpl
//@formatter:on
)
return
}
}
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
//@formatter:on
)
return
}
}
}

@pure def pushWithinCapacity[T](q: Queue[T], a: T): Unit = {
Contract(
Requires(q.length < q.capacity),
Ensures(q.push(a).buffer ≡ (q.buffer ++ List.make(a)))
)

q.strategy match {
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
//@formatter:on
)
return
}
case Queue.Strategy.DropLatest => {
Deduce(
//@formatter:off
1 ( q.length < q.capacity ) by Premise,
2 ( q.strategy == List.Queue.Strategy.DropLatest ) by Auto,
3 ( q.push(a).buffer ≡ (q.buffer ++ List.make(a)) ) by Simpl
//@formatter:on
)
return
}
case Queue.Strategy.Error => {
Deduce(
//@formatter:off
1 ( q.length < q.capacity ) by Premise,
2 ( q.strategy == List.Queue.Strategy.Error ) by Auto,
3 ( q.push(a).buffer ≡ (q.buffer ++ List.make(a)) ) by Simpl
//@formatter:on
)
return
}
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).buffer ≡ (q.buffer ++ List.make(a)) ) by Simpl
//@formatter:on
)
return
}
}
}
}


Expand Down
13 changes: 6 additions & 7 deletions shared/src/main/scala/org/sireum/logika/Logika.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -145,6 +145,7 @@ object Logika {
object Info {
@enum object Kind {
"Verified"
"Error"
}
}
}
Expand Down Expand Up @@ -1501,13 +1502,11 @@ import Util._
}
return s0
} else if (!config.searchPc) {
if (config.detailedInfo) {
reporter.error(Some(pos), kind,
st"""Could not find the fact that the right-hand-side operand is non-zero in the path conditions:
|{
| ${(for (pc <- pcs) yield pc.prettyST, ";\n")}
|}""".render)
}
reporter.error(Some(pos), kind,
st"""Could not find the fact that the right-hand-side operand is non-zero in the path conditions:
|{
| ${(for (pc <- pcs) yield pc.prettyST, ";\n")}
|}""".render)
return s0(status = State.Status.Error)
}
}
Expand Down
11 changes: 7 additions & 4 deletions shared/src/main/scala/org/sireum/logika/ReporterImpl.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -112,10 +112,13 @@ final class ReporterImpl(val logPc: B,
}
}

override def inform(pos: Position, kind: Logika.Reporter.Info.Kind.Type, message: String): Unit =
if (logDetailedInfo) {
info(Some(pos), Logika.kind, message)
}
override def inform(pos: Position, kind: Logika.Reporter.Info.Kind.Type, message: String): Unit = kind match {
case Logika.Reporter.Info.Kind.Verified =>
if (logDetailedInfo) {
info(Some(pos), Logika.kind, message)
}
case Logika.Reporter.Info.Kind.Error => error(Some(pos), Logika.kind, message)
}

override def illFormed(): Unit = {
}
Expand Down
Loading

0 comments on commit fa1b543

Please sign in to comment.