Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Make arrow types not look like reference types for the resolver | 2014-08-14 | |
| | |||
* | Optimise ApplyExpr to FunctionCallExpr when possible in translator | 2014-08-14 | |
| | |||
* | Generate function handle requires for functions without a body | 2014-08-14 | |
| | |||
* | Reword error message for type error in lambda requires clause | 2014-08-14 | |
| | |||
* | Fix bug in type substitution for type variables | 2014-08-14 | |
| | |||
* | Allow reads to take fields of type A -> set<object> | 2014-08-14 | |
| | |||
* | Refactor: Change ApplyExpr's Receiver to Function | 2014-08-14 | |
| | |||
* | Add lambda compilation example, and remove some unused files from the tests | 2014-08-13 | |
| | |||
* | Re-included lost calls to CheckEqualityTypes_Type | 2014-08-13 | |
| | | | | Modified syntax in some tests, since predicates now require parentheses (without parentheses refers to a predicate, not an application of the predicate) | ||
* | Merge | 2014-08-13 | |
|\ | |||
* | | Check for proper use of equality-supporting types also in local variables ↵ | 2014-08-13 | |
| | | | | | | | | and forall statements, and more expressions | ||
| * | Addressed CodeContract complaint about purity | 2014-08-12 | |
| | | |||
| * | Rewrote two tests to make triggering better (while waiting for better ↵ | 2014-08-12 | |
| | | | | | | | | automatic triggering support in either Dafny or Boogie) | ||
| * | Forget the extra copy of DafnyRuntime.cs that gets copied into DafnyExtension | 2014-08-12 | |
| | | |||
| * | Compile lambda functions and apply expressions, and change let expr compilation | 2014-08-12 | |
| | | |||
| * | Merge | 2014-08-11 | |
| |\ | |/ |/| | |||
| * | Add higher-order-functions and some other goodies | 2014-08-11 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * The reads clause now needs to be self framing. * The requires clause now needs to be framed by the reads clause. * There are one-shot lambdas, with a single arrow, but they will probably be removed. * There is a {:heapQuantifier} attribute to quantifiers, but they will probably be removed. * Add smart handling of type variables * Add < and > for datatype & type parameter | ||
* | | Merge | 2014-08-05 | |
|\ \ | |||
* | | | Resolved further merge issues | 2014-08-05 | |
| | | | |||
| * | | Tests for non-terminating computations. Already passing. | 2014-08-05 | |
| | | | |||
* | | | Merge | 2014-08-02 | |
|\| | | |||
* | | | Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in ↵ | 2014-08-02 | |
| | | | | | | | | | | | | the resolver and translator | ||
| * | | added one more test case | 2014-07-31 | |
| | | | |||
| * | | combined few tests | 2014-07-31 | |
| | | | |||
| * | | combined two tests | 2014-07-31 | |
| | | | |||
| * | | Merge | 2014-07-31 | |
| |\ \ | |||
| | * | | Changed test case to not use '/doNotUseParallelism' anymore. | 2014-07-31 | |
| | |/ | |||
* | | | Test file whitespace delta | 2014-07-23 | |
| | | | |||
* | | | Implemented missing routine in runtime system (real-to-int conversion) | 2014-07-21 | |
| |/ |/| | |||
| * | added one more test. | 2014-07-20 | |
| | | |||
| * | - fixed a bug in inheriting members from a trait | 2014-07-20 | |
| | | | | | | | | | | | | | | => ResolvedClass in userdefinedtypes used to be null-> fixed - checking only bodyless methods and functions to make sure they have been implemented in the child class - added one more test | ||
| * | fixed one .expect file. now all 11 tests related to Traits pass. | 2014-07-20 | |
| | | |||
| * | - fixed an issue regarding including ghost functions in the compiled interface | 2014-07-20 | |
| | | | | | | | | - added one more test | ||
| * | added ignored files | 2014-07-18 | |
| | | |||
| * | added trait feature: | 2014-07-18 | |
|/ | | | | | | -possibility to declare traits in Dafny -possibility to extend a class by a trait -possibility to override body-less methods | ||
* | Fixed build break from recent change | 2014-07-15 | |
| | |||
* | An attempt at making dafny4/NumberRepresentations.dfy run faster and more ↵ | 2014-07-15 | |
| | | | | predictably | ||
* | Renamed "arbitrary type" to "opaque type" | 2014-07-15 | |
| | |||
* | Allow an arbitrary-type to take type parameters | 2014-07-15 | |
| | |||
* | Added more tests. | 2014-07-15 | |
| | |||
* | Another variation of GenericSort, this time instantiating with "int" | 2014-07-14 | |
| | |||
* | Merge | 2014-07-14 | |
|\ | |||
* | | Support for type synonyms in refinements | 2014-07-14 | |
| | | | | | | | | Started allowing arbitrary types to have type parameters | ||
| * | Added a test. | 2014-07-13 | |
|/ | |||
* | Merge | 2014-07-11 | |
|\ | |||
* | | Added type synonyms. (No support yet for these in refinements.) | 2014-07-11 | |
| | | |||
| * | Check that type arguments to map display expressions are fully resolved | 2014-07-11 | |
| | | | | | | | | Also add a test case for the different display expressions. | ||
| * | Don't assume can calls for quantifiers | 2014-07-11 | |
|/ | | | | Fixes regression in Cyclic in Floyd Cycle Detection. | ||
* | Make reveal axioms from opaque functions quantify over layers | 2014-07-10 | |
| | |||
* | Added more tests for the more advanced verification result caching. | 2014-07-10 | |
| |