Leon

import leon.lang._ import leon.lang.synthesis._ import leon.annotation._ object Delete { sealed abstract class List case class Cons(head: Int, tail: List) extends List case object Nil extends List def size(l: List) : Int = (l match { case Nil => 0 case Cons(_, t) => 1 + size(t) }) ensuring(res => res >= 0) def content(l: List): Set[Int] = l match { case Nil => Set.empty[Int] case Cons(i, t) => Set(i) ++ content(t) } def insert(in1: List, v: Int): List = { Cons(v, in1) } ensuring { content(_) == content(in1) ++ Set(v) } def delete(in1: List, v: Int) = choose { (out : List) => content(out) == content(in1) -- Set(v) } }

    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 v2.2-da00c47 © EPFL, Lausanne 2009-2014