Leon

import leon.lang._ import leon.annotation._ object AmortizedQueue { sealed abstract class List case class Cons(head : BigInt, tail : List) extends List case object Nil extends List sealed abstract class AbsQueue case class Queue(front : List, rear : List) extends AbsQueue def size(list : List) : BigInt = (list match { case Nil => 0 case Cons(_, xs) => 1 + size(xs) }) ensuring(_ >= 0) def content(l: List) : Set[BigInt] = l match { case Nil => Set.empty[BigInt] case Cons(x, xs) => Set(x) ++ content(xs) } def asList(queue : AbsQueue) : List = queue match { case Queue(front, rear) => concat(front, reverse(rear)) } def concat(l1 : List, l2 : List) : List = (l1 match { case Nil => l2 case Cons(x,xs) => Cons(x, concat(xs, l2)) }) ensuring (res => size(res) == size(l1) + size(l2) && content(res) == content(l1) ++ content(l2)) def isAmortized(queue : AbsQueue) : Boolean = queue match { case Queue(front, rear) => size(front) >= size(rear) } def isEmpty(queue : AbsQueue) : Boolean = queue match { case Queue(Nil, Nil) => true case _ => false } def reverse(l : List) : List = (l match { case Nil => Nil case Cons(x, xs) => concat(reverse(xs), Cons(x, Nil)) }) ensuring (content(_) == content(l)) def amortizedQueue(front : List, rear : List) : AbsQueue = { if (size(rear) <= size(front)) Queue(front, rear) else Queue(concat(front, reverse(rear)), Nil) } ensuring(isAmortized(_)) def enqueue(queue : AbsQueue, elem : BigInt) : AbsQueue = (queue match { case Queue(front, rear) => amortizedQueue(front, Cons(elem, rear)) }) ensuring(isAmortized(_)) def tail(queue : AbsQueue) : AbsQueue = { require(isAmortized(queue) && !isEmpty(queue)) queue match { case Queue(Cons(f, fs), rear) => amortizedQueue(fs, rear) } } ensuring (isAmortized(_)) def front(queue : AbsQueue) : BigInt = { require(isAmortized(queue) && !isEmpty(queue)) queue match { case Queue(Cons(f, _), _) => f } } @induct def propFront(queue : AbsQueue, list : List, elem : BigInt) : Boolean = { require(!isEmpty(queue) && isAmortized(queue)) if (asList(queue) == list) { list match { case Cons(x, _) => front(queue) == x } } else true } holds def enqueueAndFront(queue : AbsQueue, elem : BigInt) : Boolean = { if (isEmpty(queue)) front(enqueue(queue, elem)) == elem else true } holds def enqueueDequeueThrice(queue : AbsQueue, e1 : BigInt, e2 : BigInt, e3 : BigInt) : Boolean = { if (isEmpty(queue)) { val q1 = enqueue(queue, e1) val q2 = enqueue(q1, e2) val q3 = enqueue(q2, e3) val e1prime = front(q3) val q4 = tail(q3) val e2prime = front(q4) val q5 = tail(q4) val e3prime = front(q5) e1 == e1prime && e2 == e2prime && e3 == e3prime } else true } holds }

    Load a Program:

    Analysis

    Synthesis

    Console:

    Features:

    ×

    Failed to connect

    The Leon server appears to be unreachable right now.

    ×

    Failed to connect

    Leon failed to contact the mothership :(

    It usually indicates that your firewall blocks traffic on websocket ports.

    Leon-978a08c (Built 2015-05-13) © EPFL, Lausanne 2009-2015