summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Dafny: added Carrol Morgan's calculator regression test.Gravatar kyessenov2010-07-02
* Dafny: support input/output parameters in refined methods.Gravatar kyessenov2010-07-02
* Dafny: added a regression test for the refinement extension.Gravatar kyessenov2010-07-02
* Added a simple refinement extension to Dafny. The new keywords are "refines" ...Gravatar kyessenov2010-07-02
* Boogie: Fixed the build.Gravatar wuestholz2010-07-02
* These 2 files are remnants of attempting the earlier planned method of renami...Gravatar tabarbe2010-07-01
* As it turns out, the C# Intellisense compiler takes precedence over the Spec#...Gravatar tabarbe2010-07-01
* I am working to port Boogie from Spec# to C#. As part of this process, I nee...Gravatar tabarbe2010-06-30
* (no commit message)Gravatar tabarbe2010-06-30
* Forgotten file.Gravatar mikebarnett2010-06-30
* (no commit message)Gravatar tabarbe2010-06-29
* (no commit message)Gravatar tabarbe2010-06-29
* (no commit message)Gravatar tabarbe2010-06-29
* (no commit message)Gravatar tabarbe2010-06-29
* (no commit message)Gravatar tabarbe2010-06-29
* (no commit message)Gravatar tabarbe2010-06-29
* (no commit message)Gravatar tabarbe2010-06-29
* (no commit message)Gravatar tabarbe2010-06-29
* (no commit message)Gravatar tabarbe2010-06-29
* (no commit message)Gravatar tabarbe2010-06-29
* (no commit message)Gravatar tabarbe2010-06-29
* Testing whether history of an old file remains after rename and commit.Gravatar tabarbe2010-06-29
* Simplified the translator by merging the ToplevelTraverser, ClassTraverser, a...Gravatar mikebarnett2010-06-28
* Chalice:Gravatar rustanleino2010-06-25
* Chalice: Applied patch #6192Gravatar mueller2010-06-25
* Unified the .frame files so that both Boogie and Dafny use exactly the same o...Gravatar mikebarnett2010-06-25
* slightly improved syntax fileGravatar kyessenov2010-06-24
* Dafny:Gravatar rustanleino2010-06-24
* Dafny:Gravatar rustanleino2010-06-24
* Updated the frame files to work with the latest Coco/R. This entails *not* ha...Gravatar mikebarnett2010-06-22
* Boogie:Gravatar rustanleino2010-06-22
* VIM syntax file for BPL. I just had it laying around.Gravatar MichalMoskal2010-06-21
* A simple highlighting syntax file for Vim.Gravatar kyessenov2010-06-21
* Dafny:Gravatar rustanleino2010-06-19
* Dafny:Gravatar rustanleino2010-06-18
* Added the factory pattern so that all traversers are created through factory ...Gravatar mikebarnett2010-06-16
* Derive IsabelleContext from DeclFreeProverContextGravatar stobies2010-06-16
* Improved error messages for doomed program points.Gravatar schaef2010-06-15
* Dafny:Gravatar rustanleino2010-06-14
* Dafny: Added two additional heuristics for guessing missing loop decreases c...Gravatar rustanleino2010-06-11
* fixed a compiler warning about initialization of a non-null field inside the ...Gravatar qadeer2010-06-10
* Dafny: Another bug fix in SplitExpr, having to do with generic results of fu...Gravatar rustanleino2010-06-09
* Chalice: fixed bug in the exhale of permissions (to handle negative epsilons)Gravatar mueller2010-06-09
* Dafny: Fix type bug in SplitExpr translation.Gravatar rustanleino2010-06-08
* Dafny: For functions with an empty decreases clause that use the reads clause...Gravatar rustanleino2010-06-08
* Boogie:Gravatar rustanleino2010-06-08
* Consistently use the new code pattern for translating locations to tokens and...Gravatar mikebarnett2010-06-07
* Added forgotten file.Gravatar mikebarnett2010-06-06
* Updated the project to .NET v4.0.Gravatar mikebarnett2010-06-06
* Dafny:Gravatar rustanleino2010-06-05