index
:
debian-dafny
master
Debian packaging for Dafny
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Test
Commit message (
Expand
)
Author
Age
*
GHC-MergeSort: removed lemmas and proof steps rendered unnecessary now that a...
Rustan Leino
2014-01-09
*
Dafny renditions of sorting algorithms proved in other provers (Coq, Isabelle...
Rustan Leino
2014-01-08
*
Merge
Rustan Leino
2014-01-08
|
\
*
|
Allow left-hand sides of a let expression to be patterns (like in the case of...
Rustan Leino
2014-01-08
|
*
:autoReq now works with static functions.
Bryan Parno
2014-01-08
|
*
Add autoReq support for matches.
Bryan Parno
2014-01-08
|
*
Added support for automatic generation of function requirements via the :auto...
Bryan Parno
2014-01-08
|
/
*
More thoroughly check for nested assume statements during compilation
Rustan Leino
2014-01-05
*
Added ghost let expressions.
Rustan Leino
2014-01-05
*
Renamed a constructor in a test file
Rustan Leino
2014-01-03
*
Removed unused declaration
Rustan Leino
2014-01-03
*
Changed BreadthFirstSearch example to no longer use "inductive naturals", seq...
Rustan Leino
2014-01-03
*
Allow "match" expressions anywhere
Rustan Leino
2014-01-03
*
Added proper parsing for StmtExpr's in all contexts.
Rustan Leino
2013-12-30
*
Add pretty-printing flag to the dafny3 test script.
wuestholz
2013-12-19
*
Added test3/GenericSort.dfy, which shows how modules can be used to write and...
Rustan Leino
2013-12-18
*
Add an assertion to a test case to make it less flaky (hopefully).
wuestholz
2013-12-18
*
Added missing file (sorry)
Rustan Leino
2013-12-18
*
Add support for the /verifySeparately flag in Boogie and change most tests to...
wuestholz
2013-12-18
*
Fixed pretty printing of calc statements to use the new(-since-long) format.
Rustan Leino
2013-12-17
*
Don't expand {:opaque} for inherited functions. (Note, more design is still ...
Rustan Leino
2013-12-17
*
Merge
Rustan Leino
2013-12-17
|
\
*
|
Don't inline opaque functions.
Rustan Leino
2013-12-17
|
*
Merge
Rustan Leino
2013-12-16
|
|
\
|
|
/
|
/
|
|
*
Fixed bug where free conditions preceded checked conditions (for inlined pred...
Rustan Leino
2013-12-16
*
|
Pass assert/assume attributes down to Boogie
Rustan Leino
2013-12-16
*
|
Add support for the :axiom attribute for ghost methods.
Bryan Parno
2013-12-13
*
|
Added support for opaque function definitions, indicated via the {:opaque} at...
Bryan Parno
2013-12-13
*
|
Add support for the "include" keyword, which accepts a (possibly relative) path
Bryan Parno
2013-12-10
*
|
Update an 'Answer' file.
wuestholz
2013-12-10
*
|
Change a test program to verify faster (by a factor of 10-25).
wuestholz
2013-12-10
*
|
Updated an 'Answer' file.
wuestholz
2013-12-03
|
/
*
Use full name of type in compilation error
Rustan Leino
2013-11-18
*
Merge
Rustan Leino
2013-11-18
|
\
|
*
Added support for attributes on variable declarations.
wuestholz
2013-11-18
*
|
Let compiler complain about body-less functions and methods, even if these ar...
Rustan Leino
2013-11-14
|
/
*
Allow calls to side-effect-free ghost methods from expressions
Rustan Leino
2013-08-06
*
Merged PredicateExpr and CalcExpr into a single StmtExpr
Rustan Leino
2013-08-06
*
Allow co-predicates to be wrapped inside bounded existential quantifiers
Rustan Leino
2013-08-04
*
Disallow call-graph clusters that mix co-methods / prefix methods with other ...
Rustan Leino
2013-08-04
*
Set up call-graph to keep track of edges between functions and methods. (To ...
Rustan Leino
2013-08-04
*
Introduced keywords "lemma" (like a "ghost method", but not allowed to have a...
Rustan Leino
2013-08-02
*
More and improved CaptureState info
Rustan Leino
2013-08-02
*
Merge
Nadia Polikarpova
2013-07-31
|
\
*
|
Allowing dangling hints in calculations.
Nadia Polikarpova
2013-07-31
|
*
Add support for hexidecimal numbers.
parno
2013-07-30
|
/
*
Co-recursion, now sounder than ever!
Rustan Leino
2013-07-30
*
Added an assert to help the theorem prover out in the RingBuffer.Enqueue method.
Rustan Leino
2013-07-29
*
Make functions and predicates be opaque outside the defining module -- only t...
Rustan Leino
2013-07-29
*
Added some test cases: theorem about infinite and finite trees.
Rustan Leino
2013-07-27
[next]