summaryrefslogtreecommitdiff
path: root/Jennisys
Commit message (Expand)AuthorAge
* - fixed some bugs with applying unification over list elementsGravatar Unknown2011-07-06
* - implemented some sorts of symbolic evaluation of expressionsGravatar Unknown2011-07-06
* - implemented synthesis of some simple constructors with parametersGravatar Unknown2011-07-05
* added some doc commentsGravatar Unknown2011-07-03
* - when analyzing a constructor, repeated "assume <inv>" statement explicitlyGravatar Unknown2011-07-02
* - generates "Valid()" for preconditionsGravatar Unknown2011-07-01
* - removed the "Constructor" discriminator from type Member, and added aGravatar Unknown2011-07-01
* fixed some minor bugs:Gravatar Unknown2011-06-24
* - implemented code generation from a synthesis solution (simple fieldGravatar Unknown2011-06-24
* - implemented reading models from a BVD model fileGravatar Unknown2011-06-24
* refactored the Analyzer code so that it generates a separate Dafny file for eachGravatar Unknown2011-06-20
* - changed the grammar to allow for arbitrary post-condition expressionsGravatar Unknown2011-06-19
* Jennisys: a (failed) attempt at getting a model from which one could generate...Gravatar Rustan Leino2011-04-22
* Jennisys: First cut of injectivity analysisGravatar Rustan Leino2011-04-11
* Jennisys: Allow model members to occur in any orderGravatar Rustan Leino2011-04-07
* Jennisys: Refined parsing of expressions, frames, and routine bodiesGravatar Rustan Leino2011-04-07
* Jennisys: Improved parsing by using operator binding powersGravatar Rustan Leino2011-04-07
* Jennisys: Parse and printGravatar Rustan Leino2011-04-07
* Jennisys: some initial files (with no real contents)Gravatar Rustan Leino2011-04-06