Clustering (--comparefuns for equivalence checking) #931
Conversation
|
|
vkuncak
changed the title
vkuncak
changed the title
| val postcondition = function.postcondition | ||
|
|
||
| val precondition = exprOps.preconditionOf(function.fullBody) //function.precondition | ||
| val postcondition = exprOps.postconditionOf(function.fullBody) //function.postcondition | ||
| val bodyPre = exprOps.withPrecondition(body, precondition) | ||
| val bodyPost = exprOps.withPostcondition(bodyPre,postcondition) |
There was a problem hiding this comment.
Could you try to manipulate specifications (getting pre/postconditions, and changing them), using the new BodyWithSpecs API?
|
@drganam : I just realized that @opaque
def zero_check(arg: BigInt): Boolean = {
if (arg > 0) zero_check(arg - 1)
else true
} ensuring (res => zero1(arg) == zero2(arg)) |
|
|
||
| case Some(paths) => | ||
| // Support wildcard `_` as specified in the documentation. | ||
| // A leading wildcard is always assumes. |
|
|
||
| case Some(paths) => | ||
| // Support wildcard `_` as specified in the documentation. | ||
| // A leading wildcard is always assumes. |
There was a problem hiding this comment.
Same here for "assumes", perhaps you could factor this code into a common function
| Induction and @traceInduct annotation | ||
| ------------------------------------- | ||
|
|
||
| We introduce the @traceInduct annotation for automating proofs using induction. Stainless will transform the annotated lemma by generating the inductive proof, based on the structure of one of the functions that appear in the lemma. This approach is useful for functions that have simple inductive form and are easily mapped into inductive proofs. |
There was a problem hiding this comment.
You can surround @traceInduct (and other code) with backquotes like this ``@traceInduct``.
|
@jad-hamza @vkuncak the latest implementation (with |
Introduces two command line options: --comparefuns and --models, for equivalence checking of specified functions