Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 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 | |
| | |||
* | 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 | |
| | | |||
| * | 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 | ||
* | | Resolved further merge issues | 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 | ||
| * | - 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 an issue regarding including ghost functions in the compiled interface | 2014-07-20 | |
| | | | | | | | | - added one more test | ||
| * | 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 | |
| | |||
* | Renamed "arbitrary type" to "opaque type" | 2014-07-15 | |
| | |||
* | Allow an arbitrary-type to take type parameters | 2014-07-15 | |
| | |||
* | Support for type synonyms in refinements | 2014-07-14 | |
| | | | | Started allowing arbitrary types to have type parameters | ||
* | 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 | |
| | |||
* | Worked on the more advanced verification result caching. | 2014-07-10 | |
| | |||
* | Worked on the more advanced verification result caching. | 2014-07-10 | |
| | |||
* | Merge | 2014-07-09 | |
|\ | |||
* | | Ignore checked-only and free-only split expressions in places where they ↵ | 2014-07-09 | |
| | | | | | | | | | | | | "don't belong". (This currently breaks dafny0/FunctionSpecifications.dfy and cloudmake/CloudMake-CachedBuilds.dfy, but a fix for those is underway.) | ||
| * | Worked on the more advanced verification result caching. | 2014-07-09 | |
|/ | |||
* | Build VS Extension for both VS 2012 and VS 2013. | 2014-07-08 | |
| | | | | Currently builds only in VS 2012. To build in VS 2013, change MinimumVisualStudioVersion from 11.0 to 12.0 in these two .csproj files. | ||
* | Further resolved merge conflicts | 2014-07-08 | |
| | |||
* | Merge | 2014-07-08 | |
|\ | |||
* | | Implemented compilation of the int<->real conversions, and changed the ↵ | 2014-07-08 | |
| | | | | | | | | | | | | resolution and verification implementations of these. Changed FreshExpr to be a UnaryExpr, and also introduced the UnaryOpExpr subclass. | ||
| * | Merge | 2014-07-07 | |
| |\ | |||
| * | | New logical encoding of types with Is and IsAlloc | 2014-07-07 | |
| | | | |||
| | * | Merge | 2014-07-03 | |
| | |\ | |||
| | * | | Translate CanCallAssumption with the same fuel value as in the body of the ↵ | 2014-07-03 | |
| | | | | | | | | | | | | | | | | function definition axiom (which prevents some matching loops) | ||
| | | * | Changed "dummy" checksums to "stable" and added more tests for the ↵ | 2014-07-03 | |
| | | | | | | | | | | | | | | | | verification result caching. | ||
* | | | | Fixed a crash in the translation of fresh(seq<T>). | 2014-07-02 | |
| |_|/ |/| | | |||
| | * | Merge | 2014-07-02 | |
| | |\ | |_|/ |/| | | |||
| | * | Allow array-type parameters to be filled in automatically. | 2014-07-02 | |
| | | | | | | | | | | | | Enhanced filling in of datatype parameters: allow places that need only a prefix of the parameters of the datatype | ||
* | | | DafnyExtension: Worked on adding support for Visual Studio 2013. | 2014-07-02 | |
| | | | |||
| | * | Merge | 2014-07-01 | |
| | |\ | |_|/ |/| | | |||
* | | | Dispose DafnyTokenTagger | 2014-07-01 | |
| | | | |||
* | | | Color nested comments correctly in the Dafny IDE | 2014-07-01 | |
| | | |