Comments (8)
Good catch! It's indeed not packaged... We'll fix this for the next release, but in the meantime here is a correctly packaged archive
stainless-algebra_2.13.zip (that should replace the incorrectly packaged one).
from stainless.
Hello!
One way to include the Ord
typeclass is to have it as a field in BST
:
import stainless.*
import stainless.collection.*
import stainless.algebra.*
sealed abstract class BST[V]:
val ord: TotalOrder[V] // here
// unbalanced invariant, which should be put before and after each operation method
// (having it in a require causes an unfortunate crash)
def valid: Boolean =
this match
case Empty(_) => true
case Node(l, v, r, _, _) =>
l.values.forall(ord.compare(_, v) < 0)
&& r.values.forall(ord.compare(_, v) > 0)
def values: List[V] =
this match
case Empty(_) => Nil()
case Node(l, v, r, _, _) => l.values ++ List(v) ++ r.values
def insert(v: V): BST[V] = {
require(valid)
// ...
}.ensuring(_.valid)
case class Empty[V](override val ord: TotalOrder[V]) extends BST[V]
case class Node[V](left: BST[V], data: V, right: BST[V], h: BigInt, override val ord: TotalOrder[V]) extends BST[V]
In this example, I'm using stainless.algebra.{Eq, PartialOrder, TotalOrder}
from here (which should be included explicitly when invoking Stainless).
Hope this helps! If not, please do not hesitate to comment further :)
from stainless.
Thank you for you response, I will try later.
By the way, the first idea that came to mind was to use invariant
to constrain it is ordered, because it is very simple - just left < value < right
. But I was not successful because of the below reason.
Then I tried to add require
and ensuring
into every operator, as you suggested. But I have a question - if I want to achieve the best form, is it necessary to modify the AVL constructor to private and only expose wrapped operators (e.g. insert/delete/contains)?
from stainless.
Then I tried to add require and ensuring into every operator, as you suggested. But I have a question - if I want to achieve the best form, is it necessary to modify the AVL constructor to private and only expose wrapped operators (e.g. insert/delete/contains)?
If I'm understanding correctly, it's not really required for correctness, it's just that the user may construct an AVL tree that is not valid and won't be able to call operations that require validity.
But this idea is nice to prevent "accidental" construction and avoid the user later confusion!
from stainless.
@mario-bucev Does it also crash when adding @invariant
to valid
and removing the pre/post-conditions?
sealed abstract class BST[V]:
val ord: TotalOrder[V]
@invariant
def valid: Boolean = // ...
def insert(v: V): BST[V] = {
// ...
}
}
from stainless.
Alas no, I get the same crash. It seems to be that the invariant FunDef
is not expecting a type parameter while it is being fed one (maybe some interaction with TypeEncoding
?)
from stainless.
How do I use the stainless.algebra
? I tried to follow the documentation and added it to sbt as follows:
stainlessExtraDeps ++= Seq(
"ch.epfl.lara" %% "stainless-algebra" % "0.1.2" cross(CrossVersion.for3Use2_13),
)
Then I ran sbt stainless-algebra/packageSrc
to get the sources jar and put it into the stainless folder, but it did not work. I noticed that the source jar is only 253 bytes:
ll stainless/ch/epfl/lara/stainless-algebra_2.13/0.1.2
total 24
-rw-r--r--@ 1 mingyang staff 253B May 11 23:32 stainless-algebra_2.13-0.1.2-sources.jar
-rw-r--r--@ 1 mingyang staff 281B May 11 23:25 stainless-algebra_2.13-0.1.2.jar
-rw-r--r--@ 1 mingyang staff 1.5K May 11 23:26 stainless-algebra_2.13-0.1.2.pom
from stainless.
If you are checking how to do balanced trees in Stainless, maybe you should check the previous working examples
https://github.com/epfl-lara/bolts/tree/master/data-structures/trees
from stainless.
Related Issues (20)
- MethodLifting reporting when subclasses have preconditions
- Convert throw into assert(false) HOT 7
- Error reporting from alias analysis
- PrimitiveSize functions should not be generated when termination checking is off?
- Treat the `erased` soft keyword as Stainless `@ghost`
- Well-formedness check failure when operating on an `Array` type alias
- Incorrect usage of `old` when it is not
- Unpredictable reporting on circular type classes
- StackOverflowError during Measure Inference
- Type error when @extern method's result widens ADT value HOT 2
- Missing dependencies when using bigSubstring HOT 1
- Finite sets printed in debug using curly braces instead of Set(...) HOT 2
- Egg invariant: unsatisfiable invariant of locally declared classes that depend on mutable local state HOT 1
- ADT must appear only in strictly positive positions when using Map
- Missformed SMT source, Unknown SMT term of class: class smtlib.trees.Terms$FunctionApplication HOT 8
- `unfolding` should return the return value of the function so that it is a hint for verification, and has the behaviour of the unfolded function at runtime HOT 4
- introduce `old` outside of post condition HOT 1
- Internal type error in extraction when passing anonymous trait instance to method expecting trait HOT 2
- `--functions` does not account for trait methods dependencies HOT 1
- Cache refactor to improve performance and footprint HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from stainless.