Questions tagged [leon]

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

Filter by
Sorted by
Tagged with
0 votes
1 answer
43 views

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 ...
user1868607's user avatar
  • 2,558
0 votes
1 answer
32 views

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) ...
user1868607's user avatar
  • 2,558
0 votes
1 answer
56 views

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 ...
user1868607's user avatar
  • 2,558
0 votes
1 answer
40 views

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 ...
user1868607's user avatar
  • 2,558
0 votes
1 answer
23 views

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 = ...
user1868607's user avatar
  • 2,558
0 votes
1 answer
45 views

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 ...
user1868607's user avatar
  • 2,558
0 votes
1 answer
43 views

Is there a notion of strong induction in Welder?

While working with Welder I faced the situtation where I have to proof that: if content(l1) == content(l2) and f is an idempotent, associative and commutative operator then fold(f,z,l1) = fold(f,z,...
user1868607's user avatar
  • 2,558
0 votes
1 answer
63 views

Proving properties of sets in Inox/Welder

I would like to proof some properties of sets on Inox/Welder but I'm lacking examples that help me to figure out how to do so. Say I want to proof: content(y::xs).contains(x) && x != y ==> ...
user1868607's user avatar
  • 2,558
0 votes
0 answers
547 views

Your firewall blocks traffic on websocket ports error on online service

I'm working with Leon verification system online at http://leon.epfl.ch/. I'm having problems with the connection with the following errors: Failed to connect: Leon failed to contact the mothership ...
user1868607's user avatar
  • 2,558
1 vote
1 answer
52 views

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 ) ...
Tom's user avatar
  • 904
2 votes
1 answer
101 views

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 + ...
Tom's user avatar
  • 904
3 votes
1 answer
74 views

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 ...
Eric Pony's user avatar
1 vote
1 answer
66 views

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 ...
Eric Pony's user avatar
1 vote
1 answer
70 views

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 ...
Wenguan Huang's user avatar
0 votes
1 answer
33 views

short-circuit evaluation in leon --xlang

Consider the following complicated way of negating a boolean (which depends on short-circuit evaluation): def negate(a: Boolean) = { var b = true a && { b = false; true } b } ensuring { ...
Samuel Gruetter's user avatar
0 votes
1 answer
59 views

Is it possible to have requirement on data structure in Leon?

While working on rational numbers with leon, I have to add as requirement isRational pretty much everywhere. For example: import leon.lang._ case class Rational (n: BigInt, d: BigInt) { def +(...
Hiura's user avatar
  • 3,500
-1 votes
1 answer
90 views

Leon: how to use custom `==` operator?

While working with leon and rationals, I encountered the following issue: the verification of the inverse1 function gives a counter-example but it doesn't make much sense, while inverse2 verifies. ...
Hiura's user avatar
  • 3,500
1 vote
1 answer
66 views

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 ...
Ravi Mad's user avatar
1 vote
3 answers
98 views

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-...
mdemarne's user avatar
2 votes
1 answer
95 views

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 ...
Nicolas Rouquette's user avatar
7 votes
2 answers
137 views

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 ...
vkuncak's user avatar
  • 123