| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Dafny: added assertions in the refinement obligation necessitating that the ↵ |  kyessenov | 2010-07-03 |
| | | | | | return values of concrete and abstract executions are equal. Refactored a test to simulate "static" function call. | ||
| * | Dafny: Support class type parameters in refinements. Added another ↵ | kyessenov | 2010-07-02 |
| | | | | | regression test -- a sequence refined by a singly linked list. | ||
| * | Dafny: added Carrol Morgan's calculator regression test. | kyessenov | 2010-07-02 |
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |