Questions tagged [leon]
Leon is an automated system for verifying, repairing, and synthesizing Scala programs.
21
questions
0
votes
1answer
40 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
1answer
28 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
1answer
52 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
1answer
38 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
1answer
19 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
1answer
40 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
1answer
42 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
1answer
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
0answers
531 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
1answer
48 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
1answer
100 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
1answer
72 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
1answer
64 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
1answer
67 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
1answer
32 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
1answer
57 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
1answer
86 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
1answer
60 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
3answers
93 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
1answer
80 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
1answer
130 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 ...