| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
| |
| |
| | |
not member equality)
|
| | | |
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| |
| | |
Dafny: fixed translation bug with missing match cases (where the constructor has some parameters)
Dafny: fixed translation bug where the program had forward references to members of a datatype
|
| | | |
|
| | | |
|
| | |\
| |/
|/| |
|
| | |
| |
| |
| | |
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
|
| |/
|
|
| |
functions/methods, and updated some test files accordingly (compare with changesets 1429 and 1366)
|
| |\ |
|
| | |
| |
| |
| | |
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
|
Rustan Leino
Aleksandar Milicevic
Unknown
Unknown