summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Dafny: keep counters for loops, temporary variables across two implementation...Gravatar kyessenov2010-07-07
* [Aste] Success: Committing summary due to changes.Gravatar codeplexbot2010-07-06
* Dafny:Gravatar rustanleino2010-07-06
* [Aste] Added summary.logGravatar codeplexbot2010-07-06
* Added a comment noting that this test fails with Z3 2.4.Gravatar mschwerhoff2010-07-06
* Boogie: Added an additional parameter 'defines' to the method 'BoogiePL.Parse...Gravatar wuestholz2010-07-06
* General hygiene: introduced (fixed) a helper method that creates Boogie token...Gravatar mikebarnett2010-07-05
* Cleaned up the sink: removed the OutVars, which was state the sink needed onl...Gravatar mikebarnett2010-07-05
* Forgotten file: Sink.csGravatar mikebarnett2010-07-05
* Chalice: Changed definition of waitlevel to take into account rdlock. Adapted...Gravatar mueller2010-07-03
* Dafny: added assertions in the refinement obligation necessitating that the r...Gravatar kyessenov2010-07-03
* Dafny: Support class type parameters in refinements. Added another regression...Gravatar kyessenov2010-07-02
* Introduction of the Sink: a global object that is threaded through all of the...Gravatar mikebarnett2010-07-02
* 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