index
:
debian-dafny
master
Debian packaging for Dafny
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Source
Commit message (
Expand
)
Author
Age
*
The "choose" statement, hacky and specialized as it was, is now gone. Use th...
Rustan Leino
2013-03-27
*
Replaced SuperSetBoundedPool by SubSetBoundedPool, which is much more useful ...
Rustan Leino
2013-03-27
*
Compilation of (many common) assign-such-that statements.
Rustan Leino
2013-03-26
*
Suppress compiler warnings about unreferenced labels (I hope all .NET platfor...
Rustan Leino
2013-03-26
*
Type-inference support for cardinality operator
Rustan Leino
2013-03-26
*
Merge
Rustan Leino
2013-03-25
|
\
*
|
Beefed up assign/let-such-that to generate possible witnesses for set/multise...
Rustan Leino
2013-03-25
|
*
First take on set, multiset and map cardinality.
Nadia Polikarpova
2013-03-22
|
/
*
Minor code cleanup.
Nadia Polikarpova
2013-03-21
*
Bumped version to 1.6.3.00320, to appear on rise4fun
Rustan Leino
2013-03-20
*
Merge
Nadia Polikarpova
2013-03-20
|
\
*
|
Finished support for ==# in calc, changed Paulson example to use it.
Nadia Polikarpova
2013-03-20
|
*
Added multiset update.
Nadia Polikarpova
2013-03-20
|
*
Added multiset indexing.
Nadia Polikarpova
2013-03-20
|
/
*
Added some data structure to support ==# in calculations.
Nadia Polikarpova
2013-03-20
*
Updated version to 1.6.2.00318
Rustan Leino
2013-03-18
*
Merge
Rustan Leino
2013-03-15
|
\
*
|
Fixed yield statement to process its arguments.
Rustan Leino
2013-03-15
|
*
Added explies support to calculations.
Nadia Polikarpova
2013-03-15
|
*
Added the <== operator.
Nadia Polikarpova
2013-03-14
|
/
*
Bumped version to 1.6.1, to be released as a binary and on rise4fun.
Rustan Leino
2013-03-10
*
Merge
Rustan Leino
2013-03-06
|
\
|
*
Disallow allocations in ghost contexts
Rustan Leino
2013-03-06
*
|
Set .Result field of calc even if there are 0 lines
Rustan Leino
2013-03-06
|
/
*
Renamed "parallel" statement to "forall" statement, and made the parentheses ...
Rustan Leino
2013-03-06
*
New well-formedness checks for calculations (no cascading).
Nadia Polikarpova
2013-03-05
*
Added side-effects and control-flow checks in hints.
Nadia Polikarpova
2013-03-05
*
Fixed crash in translator, having to do with recursive co-predicates.
Rustan Leino
2013-03-04
*
Merge
Rustan Leino
2013-02-21
|
\
|
*
Merge
Rustan Leino
2013-02-21
|
|
\
*
|
|
Pretty print the new parentheses-less "if" and "while" statements as such.
Rustan Leino
2013-02-21
*
|
|
Fixed let-such-that and if-then-else encodings so that they will pass the sub...
Rustan Leino
2013-02-21
*
|
|
Added Equals method on Type
Rustan Leino
2013-02-20
|
|
/
|
/
|
*
|
Support for paren-free guards in if and while statements.
Nadia Polikarpova
2013-02-15
|
*
Improved source location reported for two resolution errors
Rustan Leino
2013-02-14
|
/
*
Solved some contract violation issues.
Nadia Polikarpova
2013-02-14
*
Manual merge.
Nadia Polikarpova
2013-02-13
*
Merge
Nadia Polikarpova
2013-02-13
|
\
|
*
Frame expressions are now checked to be well formed.
Rustan Leino
2013-02-13
*
|
Minor fixes for calc expressions.
Nadia Polikarpova
2013-02-13
*
|
Merge
Nadia Polikarpova
2013-02-14
|
\
|
*
|
First take on calc expressions.
Nadia Polikarpova
2013-02-14
|
*
Report error if type of a quantified variable cannot be inferred
Rustan Leino
2013-02-11
*
|
Inferring parallel postcondition from calc.
Nadia Polikarpova
2013-02-12
*
|
Better well-formedness checks take 2: a context line (i.e. followed by ==>) s...
Nadia Polikarpova
2013-02-12
*
|
Minor cleanup.
Nadia Polikarpova
2013-02-12
*
|
Better well-formedness checks for ==> calculations: a line serves as context ...
Nadia Polikarpova
2013-02-08
*
|
Changed calc syntax (custom operators are now written before the hint)
Nadia Polikarpova
2013-02-08
*
|
"!!" can now be parsed as two "!". More concise parsing for "!in".
Nadia Polikarpova
2013-02-07
|
/
*
Disallow recursive copredicate calls in the body of let-such-that expressions.
Rustan Leino
2013-01-30
[next]