Stack Overflow
Stack Overflow

Questions tagged [leon]

Leon is an automated system for verifying, repairing, and synthesizing Scala programs.

Leon is an automated system for verifying, repairing, and synthesizing Scala programs. Leon is developed at the Swiss Federal Institute of Technology in Lausanne. The official Leon documentation together with an interactive demo are available online.

21 questions
7
votes
2 answers

How to prove size of a list in Leon?

I am trying to prove that the size (number of elements) in a list is non-negative, but Leon fails to prove it---it just times out. Is Leon really not capable of proving this property, or am I using it wrongly? My starting point is a function I read…
vkuncak
  • 123
  • 7
3
votes
1 answer

Problems with generic abstract types

I have an abstract Stack type as follows abstract class Stack[T] { def empty : Stack[T] def pop () : (Option[T], Stack[T]) def push (e : T) : Stack[T] def size : BigInt } I would like to verify that pop returns the last pushed element: //…
Eric Pony
  • 43
  • 4
2
votes
1 answer

How to set XLang in Leon online system,Is it possible?

I want to verify following code object Test { def test(a: Int): Int = { require(a > 0) var sum = 0 var i = 0 while(i < a) { sum = sum + i i = i + 1 } return sum } ensuring(res =>…
Tom
  • 904
  • 1
  • 7
  • 21
2
votes
1 answer

How to build leon for MacOSX?

I tried to follow the instructions to build leon for MacOSX (yosemite) from the README.md file on github. It worked well except that when I run the basic test, I get a problem with a scalaz3 library not found: $ ./leon…
Nicolas Rouquette
  • 428
  • 3
  • 16
1
vote
1 answer

Leon is not able to prove correctness of Simple Recursive program?

I have tried following programs in Leon object Test10 { def sum(n: Int): Int = ({ require(n >= 0) if (n == 0) 0 else sum(n-1)+1 })ensuring(res => res==n ) } Result--Successful object Test10 { def…
Tom
  • 904
  • 1
  • 7
  • 21
1
vote
1 answer

Is it possible to reason based on spec instead of the implementation?

I would like to use Leon to verify a spec without knowing the concrete implementations in advance. For example, suppose I have a sort function, as well as the definition of what a sorted list looks like: def sort (list: List[BigInt]): List[BigInt] =…
Eric Pony
  • 43
  • 4
1
vote
1 answer

why the wrongCommutative timeout in the PropositionalLogic example in Leon Online?

I was quite curious about the property of wrongCommutative in PropositionalLogic example in Leon. It seems like a correct property for me and I do not understand why it just time out in Leon. here is the…
Wenguan Huang
  • 19
  • 2
1
vote
1 answer

Why are there multiple options for the same SMT solver

In Leon verifier, why are there different options that use the same solver even when inductive reasoning happens within Leon? Eg. all the 3 options: fairz3, smt-z3 and unrollz3 seem to use a z3 solver and perform inductive reasoning in leon.
Ravi Mad
  • 48
  • 6
1
vote
3 answers

how do I build with scalac using Leon's library?

I am trying to compile my Leon code using scalac directly. Unfortunately, I was not able to properly build the Leon library on which the code depends. For instance, I have run scalac $(find ~/my-path/leon/library/ -name "*.scala" | xargs)…
mdemarne
  • 31
  • 4
0
votes
1 answer

Performing double induction in Welder

I'm trying to proof a property by double induction using Welder. The definitions are taken from here. A related question that gives more details of the theory can be found here. Anyways I just need some portion to show my problem: Basically, I'm…
user1868607
  • 2,558
  • 1
  • 17
  • 38
0
votes
1 answer

Using notI in Welder. Example contradiction proof

I have some problems while using the notI construct in Welder. Take the following as an example proof: My example uses usual lemmas about the structure of rings and a derived lemma (zeroDivisorLemma) that says that for all 'a' in the ring a0 = 0 =…
user1868607
  • 2,558
  • 1
  • 17
  • 38
0
votes
1 answer

How to declare an abstract function in Inox

I'm proving certain properties on elliptic curves and for that I rely on some functions that deal with field operations. However, I don't want Inox to reason about the implementation of these functions but to just assume certain properties on them.…
user1868607
  • 2,558
  • 1
  • 17
  • 38
0
votes
1 answer

Modelling a class hierarchy in Inox

I want to model the following Scala hierarchy in the Inox solver interface: abstract class Element() abstract class nonZero() extends Element final case class Zero() extends Element final case class One() extends nonZero() final case class notOne()…
user1868607
  • 2,558
  • 1
  • 17
  • 38
0
votes
1 answer

Defining infix operator in Welder

I have the following simplied definition of an addition operation over a field: import inox._ import inox.trees.{forall => _, _} import inox.trees.dsl._ object Field { val element = FreshIdentifier("element") val zero =…
user1868607
  • 2,558
  • 1
  • 17
  • 38
0
votes
1 answer

Using TypedADT constructs in Inox

The inox documentation states the following Inox provides the utility types TypedADTSort and TypedADTConstructor (see file inox/ast/Definitions.scala) that correspond to ADT definitions whose type parameters have been instantiated with…
user1868607
  • 2,558
  • 1
  • 17
  • 38
1
2