summaryrefslogtreecommitdiff
path: root/Test
Commit message (Expand)AuthorAge
* Added "modify" statement.Gravatar Rustan Leino2014-04-03
* Improvements in sequence axioms to make checking more automatic.Gravatar Rustan Leino2014-04-02
* Auto-set type arguments of built-in collection types, just like for user-defi...Gravatar Rustan Leino2014-03-21
* Added axiom to transfer array element-type information onto the elements them...Gravatar Rustan Leino2014-03-20
* Fixed problem with propagating allocation information about array elements.Gravatar Rustan Leino2014-03-20
* Propagate literals through equality operations.Gravatar Nada Amin2014-03-19
* MergeGravatar Rustan Leino2014-03-17
|\
* | Fixed resolution bug where "var x := x" was allowed.Gravatar Rustan Leino2014-03-17
* | AST refactoring:Gravatar Rustan Leino2014-03-17
| * MergeGravatar Nada Amin2014-03-12
| |\ | |/ |/|
| * Improve computations, in particular compositionality. Isolated useless litera...Gravatar Nada Amin2014-03-12
* | Added a test case from the ACL2 bookGravatar Rustan Leino2014-03-10
|/
* Moved the (long running) CloudMake test files to their own directoryGravatar Rustan Leino2014-02-28
* Added CloudMake formalization and proofs to the test suiteGravatar Rustan Leino2014-02-26
* Added examples mentioned in a paper on circular coinduction.Gravatar Rustan Leino2014-02-25
* Added further assistance in coming up with decreases clauses in SCCs with co-...Gravatar Rustan Leino2014-02-24
* Refactored code for dealing with SCCs in the call graph.Gravatar Rustan Leino2014-02-24
* Minor clean-up in a couple of test files.Gravatar Rustan Leino2014-02-24
* Fixed bugs in co-call checksGravatar Rustan Leino2014-02-23
* Added another colemma-calls-function-recursively testGravatar Rustan Leino2014-02-23
* Fixed some checking of recursive method/copredicate callsGravatar Rustan Leino2014-02-23
* Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -...Gravatar Rustan Leino2014-02-23
* Allow unary minus on realsGravatar Rustan Leino2014-02-13
* New test file: dafny4/NumberRepresentations.dfyGravatar Rustan Leino2014-02-13
* Added to the test suite a Dafny version of Basics.v from the "Software Founda...Gravatar Rustan Leino2014-02-13
* Fix soundness bug (Issue #9 on dafny.codeplex.com) in function axiom for lite...Gravatar Rustan Leino2014-02-13
* Updated test suite after a Boogie bug fix for realsGravatar Rustan Leino2014-02-10
* Add basic tests for realsGravatar Bryan Parno2014-02-10
* Preliminary support for reals in Dafny specs. No compiler suport yet.Gravatar Bryan Parno2014-02-10
* Added examples from the Kozen and Silva paper "Practical Coinduction".Gravatar Rustan Leino2014-02-10
* Provide more detailed feedback for errors involving if-then-elseGravatar Bryan Parno2014-02-03
* Some simplifications to the proof of GHC MergeSort.Gravatar Rustan Leino2014-02-01
* Added an alternative statement of the prime theoremGravatar Rustan Leino2014-01-24
* Fix a bug in the interaction between opaque and genericsGravatar Bryan Parno2014-01-23
* MergeGravatar Rustan Leino2014-01-14
|\
* | Improve error information by generating "Related location" information that t...Gravatar Rustan Leino2014-01-14
| * Improve autoReq's interactions with opaqueGravatar Bryan Parno2014-01-13
|/
* Proof that there is no bound on the size of prime numbersGravatar Rustan Leino2014-01-11
* Fixed spurious complaint about assignment to non-ghost variableGravatar Rustan Leino2014-01-11
* MergeGravatar Rustan Leino2014-01-11
|\
| * A better fix to deal with StaticReceiverTypes affected by autoReq.Gravatar Bryan Parno2014-01-10
* | GHC-MergeSort: removed lemmas and proof steps rendered unnecessary now that a...Gravatar Rustan Leino2014-01-09
|/
* Dafny renditions of sorting algorithms proved in other provers (Coq, Isabelle...Gravatar Rustan Leino2014-01-08
* MergeGravatar Rustan Leino2014-01-08
|\
* | Allow left-hand sides of a let expression to be patterns (like in the case of...Gravatar Rustan Leino2014-01-08
| * :autoReq now works with static functions.Gravatar Bryan Parno2014-01-08
| * Add autoReq support for matches.Gravatar Bryan Parno2014-01-08
| * Added support for automatic generation of function requirements via the :auto...Gravatar Bryan Parno2014-01-08
|/
* More thoroughly check for nested assume statements during compilationGravatar Rustan Leino2014-01-05
* Added ghost let expressions.Gravatar Rustan Leino2014-01-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 10:42:55 +0000