index
:
debian-dafny
master
Debian packaging for Dafny
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Test
/
dafny0
/
SmallTests.dfy
Commit message (
Expand
)
Author
Age
*
Stop pretty-print from emitting deprecated semi-colons.
qunyanm
2015-03-05
*
Language change: All functions and methods declared lexically outside any cla...
leino
2014-12-12
*
Resolve attributes of a forall statement only after bound variables have been...
leino
2014-10-29
*
Marked "free" as soon-to-be-deprecated
leino
2014-10-25
*
Stricter rules about that types need to be completely resolved.
leino
2014-10-08
*
Add higher-order-functions and some other goodies
Dan Rosén
2014-08-11
*
Check that type arguments to map display expressions are fully resolved
Dan Rosén
2014-07-11
*
Merge
Rustan Leino
2014-07-08
|
\
|
*
New logical encoding of types with Is and IsAlloc
Dan Rosén
2014-07-07
*
|
Fixed a crash in the translation of fresh(seq<T>).
Rustan Leino
2014-07-02
|
/
*
Set up the same test infrastructure as in Boogie.
wuestholz
2014-05-29
*
Added support for attributes on variable declarations.
wuestholz
2013-11-18
*
Replaced SuperSetBoundedPool by SubSetBoundedPool, which is much more useful ...
Rustan Leino
2013-03-27
*
Beefed up assign/let-such-that to generate possible witnesses for set/multise...
Rustan Leino
2013-03-25
*
Disallow allocations in ghost contexts
Rustan Leino
2013-03-06
*
Renamed "parallel" statement to "forall" statement, and made the parentheses ...
Rustan Leino
2013-03-06
*
Translate let-such-that expressions
Rustan Leino
2013-01-22
*
improved and fixed compilation and resolution of assign-such-that statements
Rustan Leino
2012-10-05
*
Dafny: added heuristics for finding witnesses in assign-such-that checking
Unknown
2012-08-10
*
Dafny: removed allocated, changed semantics of fresh
Jason Koenig
2012-07-29
*
Dafny: Since it's no longer true that all types support equality at run-time ...
Unknown
2012-06-21
*
Dafny: Changed the semantics of the assign-such-that statement "x :| P;" to c...
Unknown
2012-06-13
*
Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :| Expr;
Unknown
2012-03-15
*
Dafny: Fixed a bug in the pretty printer.
wuestholz
2011-12-26
*
Dafny: Extended the support for attributes on method/constructor calls.
wuestholz
2011-12-23
*
Dafny: Added support for attributes on method/constructor calls.
wuestholz
2011-12-21
*
Dafny: Added support for attributes on various specification constructs (asse...
wuestholz
2011-12-07
*
Dafny: fix bug in translation of (the splitting of) if-then-else expressions ...
Rustan Leino
2011-12-10
*
Dafny: Forward attributes on Dafny functions to Boogie (e.g., to disable well...
wuestholz
2011-12-07
*
Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" s...
Rustan Leino
2011-10-26
*
Dafny: Added support for attributes on methods and constructors.
wuestholz
2011-09-16
*
Dafny: Fixed axioms for Seq#Contains vs. the sequence building functions
Rustan Leino
2011-06-29
*
Merge
Rustan Leino
2011-05-27
|
\
|
*
Dafny: permanently changed the syntax of "datatype" declarations to what prev...
Rustan Leino
2011-05-27
*
|
Dafny: fixed bug (ill-formed Boogie) in translation of "foreach" for sequences
Rustan Leino
2011-05-26
|
*
Dafny: retired the "call" keyword
Rustan Leino
2011-05-26
|
*
Dafny:
Rustan Leino
2011-05-21
|
/
*
Dafny: Test case for sequence of boxed booleans
Rustan Leino
2011-05-16
*
Dafny: added optional range expressions to logical quantifiers, preparing for...
Rustan Leino
2011-05-15
*
Dafny: Added support for an initializing call as part of the new-allocation s...
rustanleino
2011-03-27
*
Dafny:
rustanleino
2011-02-17
*
Dafny: Added two additional heuristics for guessing missing loop decreases c...
rustanleino
2010-06-11
*
Dafny:
rustanleino
2010-05-21
*
Dafny:
rustanleino
2010-03-16
*
Dafny:
rustanleino
2010-03-16
*
Dafny: Added definedness checks for all statements (previously, some were mi...
rustanleino
2010-03-13
*
Added wellformedness checks to method specifications
rustanleino
2010-03-12
*
Dafny:
rustanleino
2010-03-12
*
Dafny: Added if-then-else expressions (replacing and extending the previous b...
rustanleino
2010-02-04
*
* Added decreases clauses to functions
rustanleino
2009-11-24
[next]