Leon

import leon.Annotations._ import leon.Utils._ 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 Results

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-e282315 © EPFL, Lausanne 2009-2014