| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
disjunction (if there is one that is true)
|
| | |
|
| |
|
|
| |
optimiations/exensions
|
| |
|
|
| |
the pre state
|
| |
|
|
|
|
| |
- updated the README.txt file with instructions on how to run examples
- added descriptions for command-line switches
- changed genMod option to be true by default
|
| |
|
|
| |
Jennisys: allow assignment statements in interfaces (for now, these are syntactic sugar for ensures clauses)
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
combinations, so now List.Find works
|
| |
|
|
| |
combinations, so now List.Find works
|
| |
|
|
|
|
|
| |
- worked on some additional list examples
- added expression simplification function
- added "decreases Repr" for recursive methods
- added desugaring when printing out method calls to Dafny
|
| |
|
|
| |
should follow soon
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
- changed the way candidate conditions are discovered; now it simply uses
all sub-expressions found in the spec that evaluate to TrueLiteral
- changed the implementation so that when trying to infer a precondition,
try out several different possibilities (and see which one works)
- added some very basic (and incomplete) type inference
- fixed a bug in the Modularizer (it didn't fix the solution after trying
out the spec infered from the solution)
- fixed a bug in DafnyModelUtils so that now when reading from the boogie
model file it keeps getting information from Seq# functions until
reaching a fixpoint (that's needed because the order or reads is important)
|
| |
|
|
|
|
|
|
|
| |
- added concreteValues field to HeapInstance
- brought back reading from Seq#Build when restoring Boogie models
- changed the how the candidate conditions are inferred: now it only
looks for unmodifiable concrete fields
- method in parameter values are added to the list of potential
candidate conditions
|
| |
|
|
|
|
|
|
| |
- changed the synthesis of the Valid() function to synthesize both unrolled
and recursive definition of it, because both are needed in certain cases
- to make the recursive definition of Valid() work, a "decreases" clause is
needed. For now, decreases clause is always "decreases Repr", and that
seems to be enough for now.
|
| |
|
|
| |
that now a simple example like Node.Tail work.
|
| |
|
|
|
|
| |
- added "modifiable objects" to heap instance
- when verifying synthesized program, only fields of the modifiable
objects are considered
|
| |
|
|
|
|
| |
infrastructural things have been implemented, like handling return parameters,
generating different "fresh" spec for methods than for constructors,
adding "Valid()" to method preconditions.
|
| |
|
|
| |
- small fixes to the modular synthesis
|
| |
|
|
|
|
| |
- moved modularization and method unification stuff to their own modules
- improved the modular synthesis so that whole branches can be delegated
to existing methods.
|
| |
|
|
| |
method that matches (specification-wise) a synthesized one
|
| |
|
|
| |
modular code
|
| |
|
|
|
|
| |
- finished the initial version of the modular code for constructors
(excluding the unification part where it tries to find an existing function
that meets the required spec)
|
| |
|
|
| |
- continued to work on the implementation of the modular code for constructors
|
| |
|
|
|
|
|
|
| |
- implemented an initial version of modular code synthesis (where the
initialization code is delegated to receiver objects instead of
modifying their private stuff directly). For now, it just generates
stub methods with appropriate specification. Another analysis can
be called for such methods to synthesize their bodies.
|
| |
|
|
|
| |
- added a rule to discover when some method arguments are equal and to use
that equality as a potential pre-condition
|
| |
|
|
|
| |
- added "inferConds" cmd line option
- refactored out some pieces of code into their own functions
|
| |
|
|
| |
ordering of field assignments
|
| |
|
|
|
|
| |
order can matter)
- fixed a bug in the piece of code for desugaring quantifiers
|
| |
|
|
|
|
|
| |
- added the following desugaring rule
forall v :: v in {a1, a2, ..., an} ==> e ~~~> e[v/a1] && e[v/a2] && ... && e[v/an]
- added the "help" command line option
|
| |
|
|
| |
- removed reading from Seq#Build because it doesn't seem to be needed anymore
|
| | |
|
| |
|
|
|
|
|
|
|
| |
and updates the Repr fields at the end of every constructor)
- refactoring:
- removed ExprConst
- change the implementation to use HeapModel and HeapInstance
(as opposed to propagating heap/env/ctx)
|
| |
|
|
| |
- added some number examples (Number.jen)
|
| | |
|
| |
|
|
|
|
|
|
| |
method arguments in method pre/post conditions and quantiication
variables in quantified expressions
- refactoring: changed the EvalSym method to return an expression instead of
a constant.
|
| | |
|
| |
|
|
| |
- some very small changes
|
| |
|
|
| |
- 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
|
| |
|
|
|
|
|
|
| |
- fixed implementation for sets
- generalized unification rules
- added command line options
- removed the "Exact" active pattern for strings (the same thing is already supported by F#)
- added a ternary if-then-else expression to Jennisys langauge and IteExpr and SetExpr to AST
|
| |
|
|
|
| |
- 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
|
| |
|
|
|
|
| |
- changed that the intermediate dafny files are written into separate
files for different method analyses
- added README and StartDafny-jen.bat
|
| |
|
|
|
|
|
| |
- 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
|
Unknown
Aleksandar Milicevic
Rustan Leino
Unknown
Unknown