index
:
debian-dafny
master
Debian packaging for Dafny
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Test
/
dafny1
Commit message (
Expand
)
Author
Age
...
*
Dafny induction:
Rustan Leino
2011-10-29
*
Dafny: continued translation of "parallel" statements (Assign and Proof forms...
Rustan Leino
2011-10-24
*
Dafny: added translation of Assign case of the parallel statement
Rustan Leino
2011-10-22
*
Dafny: beautification in one test case, and fixed an Answer file
Rustan Leino
2011-09-29
*
Dafny: added Flatten example to test suite
Rustan Leino
2011-09-11
*
Dafny: updated Answer file from recent test additions
Rustan Leino
2011-08-22
*
Dafny: updated test files (will soon update Answer files as well)
Rustan Leino
2011-08-22
*
Dafny: Fixed a bug in the printer that led to a stack overflow.
wuestholz
2011-08-11
*
Jennisys: started to work on synthesizing some methods. So far, only
Aleksandar Milicevic
2011-08-10
*
Dafny: added reverse*reverse=id example to test suite
Rustan Leino
2011-08-04
*
Dafny: re-ran parser generator to include semicolon-less body-less functions/...
Rustan Leino
2011-07-26
*
Merge
Rustan Leino
2011-07-21
|
\
*
|
Dafny: call previous lemma instead of restating it
Rustan Leino
2011-07-21
|
*
Fixed regression test failures due to removal of bodiless methods and functions.
Jason Koenig
2011-07-15
|
/
*
Dafny: allow constructors only inside classes, removed semi-colons at end of ...
Rustan Leino
2011-07-11
*
Dafny: Translate general LHSs for var and := (not yet for call, no compilatio...
Rustan Leino
2011-05-30
*
Merge
Rustan Leino
2011-05-27
|
\
|
*
Dafny: permanently changed the syntax of "datatype" declarations to what prev...
Rustan Leino
2011-05-27
|
*
Dafny:
Rustan Leino
2011-05-26
*
|
Dafny: fixed bug in induction-tactic heuristic (should never pick values whos...
Rustan Leino
2011-05-26
|
*
Dafny: retired the "call" keyword
Rustan Leino
2011-05-26
|
*
Dafny:
Rustan Leino
2011-05-21
|
/
*
Dafny: added some test cases that use nat
Rustan Leino
2011-05-16
*
Merge
Rustan Leino
2011-05-13
|
\
|
*
Dafny:
Rustan Leino
2011-05-11
*
|
Dafny: fixed compilation bugs, added @-signs in front of identifiers to avoid...
Rustan Leino
2011-05-11
|
/
*
Dafny: Fix parsing of if-then-else expressions, and don't require parentheses...
Rustan Leino
2011-04-21
*
Dafny: Alternative (and candidate replacement) syntax for declaring datatypes
Rustan Leino
2011-04-20
*
Dafny: added manual proofs for 5 theorems in Rippling.dfy
Rustan Leino
2011-04-12
*
Dafny: don't require parentheses in syntax of "choose" statements
Rustan Leino
2011-04-05
*
branch merge
Rustan Leino
2011-04-05
|
\
*
|
Dafny: Allow field selections and array-element selection as LHSs of assignme...
Unknown
2011-04-05
|
*
Dafny: fixed bug in induction over integers
Unknown
2011-04-04
|
/
*
Dafny:
rustanleino
2011-03-30
*
Dafny: Added support for an initializing call as part of the new-allocation s...
rustanleino
2011-03-27
*
Dafny: added "choose" operator on sets
rustanleino
2011-03-26
*
Dafny: improved and corrected physical/ghost distinction
rustanleino
2011-03-26
*
Dafny: compile quantifiers
rustanleino
2011-03-26
*
Dafny: Fixed typo in P16 of Rippling benchmarks, which now makes it (true and...
rustanleino
2011-03-07
*
Dafny:
rustanleino
2011-03-06
*
Dafny: Added heuristic for when to turn on the induction tactic
rustanleino
2011-03-05
*
Dafny:
rustanleino
2011-03-04
*
Dafny:
rustanleino
2011-02-17
*
Dafny: added test harness to Test/dafny1/ExtensibleArray.dfy
rustanleino
2011-02-16
*
Dafny: added ExtensibleArray program as a test
rustanleino
2011-02-16
*
Dafny: added alternate version of PriorityQueue
rustanleino
2011-02-15
*
Dafny: every decreases clause implicitly ends with a never-ending sequence of...
rustanleino
2011-02-03
*
Dafny: implemented a more precise scheme for allowing use of a function's rep...
rustanleino
2011-02-03
*
Dafny: added ensures clauses to functions
rustanleino
2011-02-02
*
Dafny: Added Test/dafny1/PriorityQueue.dfy
rustanleino
2010-12-10
[prev]
[next]