Comments (3)
I had a very brief look at it with --debug=trees
and it appears that your code is understood as:
object Preprocessing$0 {
def theorem$0(b$0 : Boolean): Unit = {
require(b$0)
check$0(b$0)
true
} ensuring {
(x$1$0 : Boolean) => true
}
() // <- Mind this part
}
and then the xlang desugaring phase will, mistakenly, keep only the check
-part. I believe the issue is linked to ExprOps.preconditionOf
and ExprOps.postconditionOf
not handling blocks as the FunDef
pre/postcondition are both None
before xlang desugaring phase.
The question is, should those functions be fixed or should such program be explicitly rejected? (It could be argued that having return type of Boolean
for a theorem is more intuitive.) Maybe @regb knows?
from leon.
Indeed the issue is that require/ensuring can be attached to any expression, and due to the Unit type and the final boolean expression, the parsed expression is a sequence of two operations:
def theorem(b: Boolean): Unit = {
val tmp = {
require(b)
check(b)
true
} ensuring {
(_ : Boolean) => true
}
()
}
And then for some reason, xlang extract the check function call without the require. That could be fixed, but then there are other issues in the solver itself, which does not seem to support require at arbitrary position in the tree.
In an ideal world we should be able to solve the solver, I don't see any issue with supporting require at any level of a function @colder @samarion @manoskouk ? But for now it's probably better to be careful and not write such functions.
from leon.
This seems like a typo to me (the return type should be Boolean), but on the subject itself:
Right now, require and ensuring are handled as pre- and postconditions of entire functions respectively. I think this is what they are meant to mean in Scala as well. If you need to state an assumption within the body of the function, one would use assume (resp. assert). Assert is already available, whereas assume is not. Introducing assume is of course possible but would be slightly complicated because we would need to check the assumption in all call sites. There are certainly a few benchmarks that could use it but it is not high in our priority list.
from leon.
Related Issues (20)
- Compilation issue HOT 2
- Termination checker unable to prove termination of mutually recursive functions HOT 1
- TODO exception with Map's and class Invariants
- leon with isabelle, undefined session, documentation HOT 4
- Prover error in operation functions: ERROR "Type unification failed: Clash of types \"<markup>\" and \"<markup>\"\n\nType error in application: incompatible operand type\n\n<markup>\n<markup>\n\n<markup>" HOT 4
- Adding ensuring(rec < ...) in a function prevents other functions from being verified
- Termination checker is unsound in handling streams
- Add doc for @traceInduct
- Bug in proofs HOT 10
- Moving to GPL from BSD HOT 2
- Bug in program evaluation/verification
- Bug in ImperativeCodeElimination
- Bug in RecursionCountInstrumenter(?)
- Z3 exception HOT 3
- Support for generic copy() method
- Can the leon library be published as a maven artifact? HOT 1
- Organization of the leon library
- Web interface appears to be failing HOT 3
- Invalid methods actually compiles
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 leon.