summaryrefslogtreecommitdiff
path: root/Test
Commit message (Collapse)AuthorAge
...
* | Start of derived types (aka "new types")Gravatar leino2014-08-20
| | | | | | | | Fixed bug in type checking for integer division.
| * MergeGravatar Rustan Leino2014-08-19
| |\ | |/ |/|
| * Change behavior of 'decreases *', which can be applied to loops and methods. ↵Gravatar Rustan Leino2014-08-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now, loops that may possibly do an infinite number of iterations (that is, loops marked with 'decreases *') and calls to methods marked with 'decreases *' are allowed only in methods that themselves are marked with 'decreases *'. As before, ghost loops and ghost methods are not allowed to be marked with 'decreases *'. Previously, 'decreases *' was allowed on a method only if the method was tail recursive; this is no longer so. Note, however, that if the method is not tail recursive and engages in infinite recursion, then it will eventually run out of stack space. Previously, a 'decreases *' was not inherited in a refining module; this is no longer so. That is, 'decreases *' is now inherited. To refine a possibly non-terminating method or loop, the refining version simply provides a decreases clause that does not mention '*'. Note that if the refined method is not recursive, it still needs to have _some_ decreases clause in order not to inherit the 'decreases *' from the refined method, but the expression stated in the decreases clause can be arbitrary (for example, one can write 'decreases true' or 'decreases 7' or 'decreases x' for some 'x' in scope). Note, in the new design, a method needs to be declared with 'decreases *' if it may recurse forever _or_ if it contains a possibly infinite loop. Note that the absence of 'decreases *' on a loop does not mean the loop will terminate, but it does mean that the loop will iterate a finite number of times (the subtle distinction here is that a loop without a 'decreases *' is allowed to contain a nested loop that has a 'decreases *' -- provided the enclosing method is also declared with 'decreases *', as previously mentioned).
* | Handle underscores in lambda bound variable lists properlyGravatar Dan Rosén2014-08-19
|/ | | | + add a test case with lambdas that don't get their types fully specified
* Fix type inference bug in data rank comparison when one side can be a TypeVarGravatar Dan Rosén2014-08-19
|
* Consider lambdas literals + create literal axioms when an argument is a functionGravatar Dan Rosén2014-08-18
|
* Add Monads as a module example and implementation of some simple monadsGravatar Dan Rosén2014-08-15
|
* Refactor resolver, and really allow reads to take fields of type A -> set<obj>Gravatar Dan Rosén2014-08-15
| | | | twoState and codeContext is moved to a new class ResolveOpts
* Add the VectorUpdate exampleGravatar Dan Rosén2014-08-14
|
* Make arrow types not look like reference types for the resolverGravatar Dan Rosén2014-08-14
|
* Reword error message for type error in lambda requires clauseGravatar Dan Rosén2014-08-14
|
* Add lambda compilation example, and remove some unused files from the testsGravatar Dan Rosén2014-08-13
|
* Re-included lost calls to CheckEqualityTypes_TypeGravatar leino2014-08-13
| | | | Modified syntax in some tests, since predicates now require parentheses (without parentheses refers to a predicate, not an application of the predicate)
* MergeGravatar leino2014-08-13
|\
* | Check for proper use of equality-supporting types also in local variables ↵Gravatar leino2014-08-13
| | | | | | | | and forall statements, and more expressions
| * Rewrote two tests to make triggering better (while waiting for better ↵Gravatar Rustan Leino2014-08-12
| | | | | | | | automatic triggering support in either Dafny or Boogie)
| * Compile lambda functions and apply expressions, and change let expr compilationGravatar Dan Rosén2014-08-12
| |
| * MergeGravatar Dan Rosén2014-08-11
| |\ | |/ |/|
| * Add higher-order-functions and some other goodiesGravatar Dan Rosén2014-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
* | MergeGravatar leino2014-08-05
|\ \
* | | Resolved further merge issuesGravatar leino2014-08-05
| | |
| * | Tests for non-terminating computations. Already passing.Gravatar Nada Amin2014-08-05
| | |
* | | MergeGravatar leino2014-08-02
|\| |
* | | Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in ↵Gravatar leino2014-08-02
| | | | | | | | | | | | the resolver and translator
| * | added one more test caseGravatar Reza Ahmadi2014-07-31
| | |
| * | combined few testsGravatar Reza Ahmadi2014-07-31
| | |
| * | combined two testsGravatar Reza Ahmadi2014-07-31
| | |
| * | MergeGravatar Reza Ahmadi2014-07-31
| |\ \
| | * | Changed test case to not use '/doNotUseParallelism' anymore.Gravatar wuestholz2014-07-31
| | |/
* | / Test file whitespace deltaGravatar leino2014-07-23
| |/ |/|
| * added one more test.Gravatar Reza Ahmadi2014-07-20
| |
| * - fixed a bug in inheriting members from a traitGravatar Reza Ahmadi2014-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.Gravatar Reza Ahmadi2014-07-20
| |
| * - fixed an issue regarding including ghost functions in the compiled interfaceGravatar Reza Ahmadi2014-07-20
| | | | | | | | - added one more test
| * added trait feature:Gravatar Reza Ahmadi2014-07-18
|/ | | | | | -possibility to declare traits in Dafny -possibility to extend a class by a trait -possibility to override body-less methods
* An attempt at making dafny4/NumberRepresentations.dfy run faster and more ↵Gravatar Rustan Leino2014-07-15
| | | | predictably
* Renamed "arbitrary type" to "opaque type"Gravatar Rustan Leino2014-07-15
|
* Allow an arbitrary-type to take type parametersGravatar Rustan Leino2014-07-15
|
* Added more tests.Gravatar wuestholz2014-07-15
|
* Another variation of GenericSort, this time instantiating with "int"Gravatar Rustan Leino2014-07-14
|
* MergeGravatar Rustan Leino2014-07-14
|\
* | Support for type synonyms in refinementsGravatar Rustan Leino2014-07-14
| | | | | | | | Started allowing arbitrary types to have type parameters
| * Added a test.Gravatar wuestholz2014-07-13
|/
* MergeGravatar Rustan Leino2014-07-11
|\
* | Added type synonyms. (No support yet for these in refinements.)Gravatar Rustan Leino2014-07-11
| |
| * Check that type arguments to map display expressions are fully resolvedGravatar Dan Rosén2014-07-11
|/ | | | Also add a test case for the different display expressions.
* Make reveal axioms from opaque functions quantify over layersGravatar Dan Rosén2014-07-10
|
* Added more tests for the more advanced verification result caching.Gravatar wuestholz2014-07-10
|
* MergeGravatar Rustan Leino2014-07-09
|\
* | Improved AnalyzeList encoding in a way that performs way better.Gravatar Rustan Leino2014-07-09
| | | | | | | | Cleaned up file to use some improved Dafny constructs.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 19:10:01 +0000