Questions tagged [leon]
Leon is an automated system for verifying, repairing, and synthesizing Scala programs.
21
questions
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 ...
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) ...
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 ...
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 ...
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 = ...
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 ...
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,...
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 ==> ...
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 ...
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 ) ...
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 + ...
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 ...
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 ...
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 ...
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 { ...
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 +(...
-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.
...
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 ...
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-...
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 ...
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 ...