| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Don't include arrow types among ordered types. |  leino | 2015-05-11 |
| | | | | | | | Fix bug with not seeing imap's because of type synonyms. Don't show semi-colon after "decreases" in hover text. Minor cosmetic change in a test case. | ||
| * | Added to the test suite a Dafny encoding of Chapter 7 from the Nipkow and ↵ | leino | 2015-05-10 |
| | | | | | | | Klein book on semantics. It includes many uses of inductive predicates and inductive lemmas. | ||
| * | Additional test case for inductive predicates | leino | 2015-05-07 |
| | | |||
| * | Added "inductive lemma" methods | leino | 2015-05-07 |
| | | |||
| * | Added inductive predicates | leino | 2015-05-06 |
| | | |||
| * | Improved generation of .reads axioms (correcting an incorrect answer and ↵ | leino | 2015-05-01 |
| | | | | | corresponding incorrectly recorded desired answer) | ||
| * | Answer file | leino | 2015-05-01 |
| | | |||
| * | Improved encoding of a property of reads clauses to make things more easily ↵ | leino | 2015-05-01 |
| | | | | | provable. | ||
| * | Added to the test suite a Dafny encoding of Chapter 3 from the Nipkow and ↵ | leino | 2015-04-29 |
| | | | | | Klein book on semantics | ||
| * | Added a test where Dafny verifies something that the Juggernaut tool can infer | leino | 2015-04-28 |
| | | |||
| * | Merge | leino | 2015-04-28 |
| |\ | |||
| * | | Changes to the VerifyThis2015 test programs | leino | 2015-04-28 |
| | | | |||
| | * | Fix issue #72. Add the constructor questionmark to a function's axiom if the | qunyanm | 2015-04-24 |
| | | | | | | | | | function has a MemberSelectExpr that accesses a type with only one constructor. | ||
| * | | Fixed bug in tuples | leino | 2015-04-24 |
| | | | |||
| | * | Fix issue #70. Check the ctors for equality before marking them as duplicates. | qunyanm | 2015-04-21 |
| | | | |||
| | * | Fix issue #73. Pass in expr.tok when creating Bpl.Expr for InMap and NotInMap. | qunyanm | 2015-04-20 |
| | | | |||
| | * | Fix issue #69. If we can't find a member in classMembers, search the static | qunyanm | 2015-04-17 |
| | | | | | | | | | members of the enclosing module or its imports. | ||
| | * | HashCode for Set/MultiSet/Map should be independent of the order of the | qunyanm | 2015-04-17 |
| | | | | | | | | | elements. | ||
| | * | Change GetHashCode for Set, MultiSet and Map | qunyanm | 2015-04-16 |
| | | | |||
| | * | Fix issue #71. When substitute the forall's variables for those of the | qunyanm | 2015-04-16 |
| | | | | | | | | | fn in fixupRevealLemma substitute the types as well. | ||
| | * | Fix issue #68. Change GetHashCode implementation for Sequence. | qunyanm | 2015-04-14 |
| |/ | |||
| * | Completed problems from the VerifyThis 2015 program verification competition | leino | 2015-04-14 |
| | | |||
| * | Fix issue #67. Check SupportsEquality before determining whether to emit Equals | qunyanm | 2015-04-13 |
| | | | | | or == for equality testing. | ||
| * | Include axioms about $Is and $IsAlloc for traits | leino | 2015-04-07 |
| | | |||
| * | Support calls to static trait methods/functions via the class | leino | 2015-04-07 |
| | | |||
| * | Revised look-up and compilation of inherited trait members (static ↵ | leino | 2015-04-07 |
| | | | | | functions/methods don't work yet) | ||
| * | Fixed compilation of static members in traits | leino | 2015-04-05 |
| | | |||
| * | Fixed some bugs in override axioms (but still missing support for classes ↵ | leino | 2015-04-05 |
| | | | | | | | | with type parameters). Resolve ClassDecl.TraitsTyp as types. Moved declaration of TraitParent and NoTraitAtAll to prelude. | ||
| * | Whitespace deltas in test files (in particular, removing tabs and adjusting ↵ | leino | 2015-04-03 |
| | | | | | some indentation) | ||
| * | Added test cases and fixes for overrides termination checks | leino | 2015-04-03 |
| | | | | | Removed syntactic presence checks for specifications--these will be checked semantically by the verifier | ||
| * | Reflect cleaner syntax in some test programs | leino | 2015-03-31 |
| | | |||
| * | Fix issue #62. Check for modifies clause and constructors in the enclosing | qunyanm | 2015-03-31 |
| | | | | | class when determining whether a method named Main() is the program entry. | ||
| * | Fix issue 61. Decreases are by default in ghost context. Therefore, | qunyanm | 2015-03-31 |
| | | | | | dontCareAboutCompilation flag should be set to false in the ResolveOpts. | ||
| * | Fix issue #56. Convert parametered opaque type parameters into an IdentifierExpr | qunyanm | 2015-03-27 |
| | | | | | instead of FunctionCall. | ||
| * | Fix issue #58. In TrSplitExpr(), add allocatedness for arguments to the inlined | qunyanm | 2015-03-26 |
| | | | | | call. | ||
| * | Fix issue #63. ForceSubstitutionOfQuantifiedVars for SetComprehesion. | qunyanm | 2015-03-17 |
| | | |||
| * | Fix issue #55 and #64. When performing type argument substitution for function | qunyanm | 2015-03-16 |
| | | | | | | | F's corresponding F_FULL, make sure the function is indeed the FullVesion before the substitution. Also keep the TypeArgsSubst for the enclosingClass in the typeMap. | ||
| * | Merge | leino | 2015-03-13 |
| |\ | |||
| * | | Allow let-such-that expression to be compiled, provided that they provably ↵ | leino | 2015-03-13 |
| | | | | | | | | | have a unique value | ||
| | * | Merge | qunyanm | 2015-03-11 |
| | |\ | |||
| | * | | Fix issue #54 and #57. Resolve a formal's type before creating a substitute. | qunyanm | 2015-03-11 |
| | | | | |||
| | | * | Beefed up collection axioms (in particular, for maps) to improve the chance ↵ | Rustan Leino | 2015-03-10 |
| | |/ |/| | | | | | of proving the existence check of let-such-that and assign-such-that | ||
| * | | Fixed bug in resolution of illegal programs. | leino | 2015-03-10 |
| | | | | | | | | | Fixed comments in some test cases. | ||
| * | | This changeset changes the default visibility of a function/predicate body ↵ | leino | 2015-03-09 |
| | | | | | | | | | | | | | | | | | | | | | outside the module that declares it. The body is now visible across the module boundary. To contain the knowledge of the body inside the module, mark the function/predicate as 'protected'. Semantics of 'protected': * The definition (i.e., body) of a 'protected' function is not visible outside the defining module * The idea is that inside the defining module, a 'protected' function may or may not be opaque. However, this will be easier to support once opaque/reveal are language primitives. Therefore, for the time being, {:opaque} is not allowed to be applied to 'protected' functions. * In order to extend the definition of a predicate in a refinement module, the predicate must be 'protected' * The 'protected' status of a function must be preserved in refinement modules | ||
| * | | Added 'protected' keyword (syntax) | leino | 2015-03-07 |
| |/ | |||
| * | Fix issue #60 | qunyanm | 2015-03-06 |
| | | |||
| * | Stop pretty-print from emitting deprecated semi-colons. | qunyanm | 2015-03-05 |
| | | |||
| * | Add imap display/update expressions | chrishaw | 2015-02-27 |
| | | |||
| * | Add imap type, which is like map but may have have infinite size | chrishaw | 2015-02-26 |
| | | |||
| * | Generate unique IDs hierarchically, to reduce changes to IDs when the ↵ | leino | 2015-01-28 |
| | | | | | program is modified (to help with fine-grained caching) | ||
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |