diff options
author | 2009-11-06 22:00:56 +0000 | |
---|---|---|
committer | 2009-11-06 22:00:56 +0000 | |
commit | 61993a0cf682448770a0e3223ba560171635c3af (patch) | |
tree | acb6a9b7af1dd7c1743c301bb4d8d0f6a4cc4ce2 /Dafny/Dafny.atg | |
parent | 68e0ee8b29d4eb06e0f2e5ac2fb13d0f05c15d13 (diff) |
Redesigned the encoding of Dafny generics, including the built-in types set and seq.
Regrettably, these changes--although improvements in Dafny's functionality--have caused Test/dafny0/BinaryTree.bpl and Test/dafny0/SchorrWaite.dfy to be significantly slower (the dafny0 test directory now takes 6:11 whereas it used to take 1:43).
Improved some of the VSI-Benchmarks to use generics more fully, where the previous designed had just crashed.
Included the previously commented-out loop invariants and assertions in VSI-Benchmarks/b8.dfy.
Added a space in the pretty printing of Boogie coercion expressions.
Diffstat (limited to 'Dafny/Dafny.atg')
0 files changed, 0 insertions, 0 deletions