| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
| |
- added examples from the oopsla submission;
- changed the default configuration not to synthesize modular code;
- changed the fixpoint solver to do more stuff in a single step, so that
only 2 iterations are needed for the examples from the paper
|
| |
|
|
|
|
| |
order can matter)
- fixed a bug in the piece of code for desugaring quantifiers
|
| |
|
|
| |
- started to work on infering branches
|
| |
|
|
|
| |
- changed Dafny so that it returns an exit code
- changed CheckDafnyProgram so that it checks Dafny exit code as well
|
| |
|
|
|
| |
- generalized the AstUtils.EvalSym functions and made the Resolver.Eval
function re-use it.
|
| |
|
|
|
|
| |
- fixed the List.jen example (generic list)
- changed SeqConst and SetConst to contain a list/set of "Const"
and not "Const option" like before
|
| |
|
|
|
|
|
| |
- added some desugaring to help the verifier. Expression like
lst = [p] + [q r]
are desugared into
lst = [p] + [q r] && lst[0] = p && lst[1] = q && lst[2] = r
|
| | |
|
| |
|
|
|
|
| |
since "assume Valid()" doesn't always work
- added optional verification step after code has been synthesized
|
| |
|
|
|
| |
- it first creates an empty model file before running Dafny
- Resolving lists used to reverse the list
|
| |
|
|
| |
assignments only), along with resolving some values missing in the model.
|
| |
|
Rustan Leino
Unknown
Unknown