Leon

Undo Redo Link Console Params About Documentation WebBuilder
Login
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
import leon.lang._
import leon.lang.synthesis._
import leon.annotation._
object Insert {
  sealed abstract class List
  case class Cons(head: BigInt, tail: List) extends List
  case object Nil extends List
  def size(l: List) : BigInt = (l match {
    case Nil => BigInt(0)
    case Cons(_, t) => 1 + size(t)
  }) ensuring(res => res >= 0)
  def content(l: List): Set[BigInt] = l match {
    case Nil => Set.empty[BigInt]
    case Cons(i, t) => Set(i) ++ content(t)
  }
  def insert(in1: List, v: BigInt) = {
    choose { (out : List) =>
      content(out) == content(in1) ++ Set(v)
    }
  }
}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

    Load an example

    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-f42327656 (Built 2017-02-03) © EPFL, Lausanne 2009-2015