summaryrefslogtreecommitdiff
path: root/Source/Dafny/DafnyAst.cs
Commit message (Collapse)AuthorAge
* Fix issue 75. Adjust the fuel for existentials to use more fuel in an assumeGravatar qunyanm2016-03-31
| | | | context and less in an assert.
* Fix issue 125. Add the missing case 2 and 3 with refinement and opened imports.Gravatar qunyanm2016-02-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For the following situation module LibA { // ...things declared here... } module LibB { // ...things declared here... } module R { import opened LibA // ...things declared here... } module S refines R { import opened LibB // ...declared here... } 1. If module R declares a TopLevelDecl “G”, then we should report an error if S attempts to declare an incompatible TopLevelDecl “G”. Dafny does this already. 2. If LibA declares a TopLevelDecl “G” but R does not directly declare any TopLevelDecl G”, then we should also issue an error for any TopLevelDecl “G” in S. This behavior is missing in Dafny. 3. If each of LibA and LibB declares some TopLevelDecl “G”, but neither R nor S directly declares any TopLevelDecl “G”, then no error should be issued, and any use of “G” in S should resolve to the “G” in LibA. This behavior is missing in Dafny.
* Implement module export so we can export a subset of items defined in theGravatar qunyanm2016-01-29
| | | | module.
* Implement 'extern' declaration modifier.Gravatar Richard L. Ford2016-01-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The 'extern' declaration modifier provides a more convenient way of interfacing Dafny code with C# source files and .Net DLLs. We support an 'extern' keyword on a module, class, function method, or method (cannot extern ghost). We check the CompileNames of all modules to make sure there are no duplicate names. Every Dafny-generated C# class is marked partial, so it can potentially be extended. The extern keyword could be accompanied by an optional string naming the corresponding C# method/class to connect to. If not given the name of the method/class is used. An 'extern' keyword implies an {:axiom} attribute for functions and methods, so their ensures clauses are assumed to be true without proof. In addition to the .dfy files, the user may supply C# files (.cs) and dynamic linked libraries (.dll) on command line. These will be passed onto the C# compiler, the .cs files as sources, and the .dll files as references. As part of this change the grammar was refactored some. New productions are - TopDecls - a list of top-level declarations. - TopDecl - a single top-level declaration - DeclModifiers - a list of declaration modifiers which are either 'abstract', 'ghost', 'static', 'protected', or 'extern'. They can be in any order and we diagnose duplicates. In addition, since they are not all allowed in all contexts, we check and give diagnostics if an DeclModifier appears where it is not allowed.
* Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so thatGravatar qunyanm2015-11-25
| | | | the auto-triggers can be computed for ForallStmt.
* Fix issue 94. Allow tuple-based assignment in statement contexts.Gravatar qunyanm2015-11-14
|
* Fix issue 101. Instead of swapping operands for Exp opcode in BinaryExpr,Gravatar qunyanm2015-11-10
| | | | | swap them when the expr is first created in parser or for calcstmt. This avoids problems of operands being swapped again when the expr is copied.
* Fix issue 104. Use ResolvedExpression to compute subexpressions forGravatar qunyanm2015-11-04
| | | | DatatypeUpdateExpr if ResovedExpression is not null.
* Introduced new datatype update syntax: D.(f := E)Gravatar leino2015-10-23
| | | | | The old syntax, D[f := E], is still supported for a short while, but generates a warning about that syntax being deprecated. The new syntax also supports multiple updates: D.(f := E0, g := E1, h := E2)
* Improve Dafny's ability to find fueled functions by checking the function ↵Gravatar Bryan Parno2015-10-19
| | | | | | itself, as well as the signature and body of other functions.
* Implemented resolution, verification, and (poorly performing) compilation of ↵Gravatar leino2015-10-05
| | | | | | | existential if guards. Fixed bugs in ghost checks involving comprehensions and attributes. Added SubstituteBoundedPool method.
* Parsing and pretty printing of the new "existential guards" of the two kinds ↵Gravatar leino2015-10-03
| | | | of "if" statements.
* MergeGravatar leino2015-09-28
|\
* | Changed computation of ghosts until pass 2 of resolution.Gravatar leino2015-09-28
| | | | | | | | | | | | | | Other clean-up in resolution passes, like: Include everything of type "char" into bounds that are discovered, and likewise for reference types. Allow more set comprehensions, determining if they are finite based on their argument type. Changed CalcExpr.SubExpressions to not include computed expressions.
| * fixed bugs related to identifying newtypes as types of integers and reals.Gravatar Michael Lowell Roberts2015-09-23
| |
* | Removed unused code (old code from previous ghost-statement handling)Gravatar leino2015-09-21
| |
| * merged IronDafny updates. two unit tests related to traits do not pass if ↵Gravatar Michael Lowell Roberts2015-09-21
| | | | | | | | ENABLE_IRONDAFNY is defined but this isn't critical and will be addressed shortly.
* | Preliminary refactoring of ghost-statement computations to after type checkingGravatar leino2015-09-20
|/
* Improve the redundancy detection algorithm used while constructing sets of termsGravatar Clément Pit--Claudel2015-08-26
| | | | | | | | Based on an issue noted by Chris with redundancy removal resuls being dependent on the order of the terms. Interestingly, one of our tests already had an instance of that problem. Also fix the issue with nested quantifiers getting redundant triggers.
* Make quantifier splitting a two step processGravatar Clément Pit--Claudel2015-08-23
| | | | This fixes a bug that affected Monad.dfy
* Grant "wishlist/useless-casts-in-decreases-clauses.dfy"Gravatar Clément Pit--Claudel2015-08-22
|
* MergeGravatar Clément Pit--Claudel2015-08-21
|\
* | Cleanup a number of FIXMEs that I had left in the codeGravatar Clément Pit--Claudel2015-08-20
| |
| * MergeGravatar Rustan Leino2015-08-20
| |\ | |/ |/|
| * Fixed compilation that involve enumeration over native-type newtype values.Gravatar Rustan Leino2015-08-20
| |
* | Merge.Gravatar Clément Pit--Claudel2015-08-20
|\|
| * MergeGravatar Rustan Leino2015-08-20
| |\
* | | Factor out some AST visiting codeGravatar Clément Pit--Claudel2015-08-19
| |/ |/|
| * Refactored and improved bounds discoveryGravatar Rustan Leino2015-08-19
| |
* | Merge.Gravatar Clément Pit--Claudel2015-08-19
|\| | | | | | | | | Changes that were needed included preventing the InductionRewriter from iterating on a SplitQuantifier and using the new error reporting engine.
* | Check Reads and Decreases clauses for expressions that could prevent inliningGravatar Clément Pit--Claudel2015-08-18
| |
| * Update the way bounds are discovered to try to choose "better" bounds.Gravatar Bryan Parno2015-08-17
| |
* | Review preceding commit with RustanGravatar Clément Pit--Claudel2015-08-17
| |
* | Start committing split quantifiersGravatar Clément Pit--Claudel2015-08-14
| | | | | | | | | | | | | | | | | | This requires rewriting the parts of the AST that contain these quantifiers. We unfortunately don't have facilities to do such rewrites at the moment (and there are loops in the AST, so it would be hard to write such a facility). As a workaround, this commit introduces a field in quantifier expressions, SplitQuantifiers. Code that manipulate triggers is expected to look for this field, and ignore the other fields if that one is found.
* | Refactor the error reporting codeGravatar Clément Pit--Claudel2015-08-18
| | | | | | | | | | The new error reporting system has a simpler interface, isn't tied to the resolver, and contains error source information.
* | Add a few utility methods to the visitorsGravatar Clément Pit--Claudel2015-08-12
| |
| * Removed the unused type ThisSurrogateGravatar leino2015-08-11
| |
| * Added routine OneAttributeToString to pretty printerGravatar leino2015-08-10
|/
* Add calc's attributes to its SubExpressions.Gravatar Clément Pit--Claudel2015-07-20
|
* Merge my autoTriggers work into the master branchGravatar Clément Pit--Claudel2015-07-17
|\ | | | | | | | | This contains trigger related things under the autoTriggers flag (disabled by default), and some bug-fixes and cleanups that are already enabled.
* | Make attributes enumerable.Gravatar Clément Pit--Claudel2015-07-13
| | | | | | | | Use an extension method to properly deal with null attributes
| * [IronDafny] implemented workaround for "import opened" bug(s).Gravatar Michael Lowell Roberts2015-07-13
| |
| * Fixed crashes in overrides checking of function decreases clauses, and ↵Gravatar Rustan Leino2015-07-07
| | | | | | | | improved the error message reported to users
* | Small refactoring of Printer.csGravatar Clément Pit--Claudel2015-07-06
| |
| * multiple changes...Gravatar Michael Lowell Roberts2015-07-02
| | | | | | | | | | - fix for requirement inheritance in refinement. - minimimally viable implementation of exclusive refinement feature.
| * Made code contracts compliantGravatar leino2015-07-01
| |
| * Add the ability to specify how much "fuel" a function should have,Gravatar Bryan Parno2015-07-01
|/ | | | | | | | | | | | | | | | | | | i.e., how many times Z3 is permitted to unfold it's definition. The new {:fuel} annotation can be added to the function itself, it which case it will apply to all uses of that function, or it can overridden within the scope of a module, function, method, iterator, calc, forall, while, assert, or assume. The general format is: {:fuel functionName,lowFuel,highFuel} When applied as an annotation to the function itself, omit functionName. If highFuel is omitted, it defaults to lowFuel + 1. The default fuel setting for recursive functions is 1,2. Setting the fuel higher, say, to 3,4, will give more unfoldings, which may make some proofs go through with less programmer assistance (e.g., with fewer assert statements), but it may also increase verification time, so use it with care. Setting the fuel to 0,0 is similar to making the definition opaque, except when used with all literal arguments.
* Add an infinite set collection type.Gravatar qunyanm2015-05-29
|
* Allow MatchExpr and MatchStmt to have nested patterns. Such asGravatar qunyanm2015-05-14
| | | | | | | | | | | | | | | | | | function last<T>(xs: List<T>): T requires xs != Nil { match xs case Cons(y, Nil) => y case Cons(y, Cons(z, zs)) => last(Cons(z, zs)) } And function minus(x: Nat, y: Nat): Nat { match (x, y) case (Zero, _) => Zero case (Suc(_), Zero) => x case (Suc(a), Suc(b)) => minus(a, b) }
* Don't include arrow types among ordered types.Gravatar leino2015-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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 06:19:56 +0000