summaryrefslogtreecommitdiff
path: root/Test/textbook
Commit message (Collapse)AuthorAge
* Added some Dafny and Boogie test cases, including Turing's factorial ↵Gravatar Rustan Leino2011-11-03
| | | | program, Hoare's classic FIND, and some induction tests for negative integers
* Miscellaneous changes:Gravatar rustanleino2010-10-22
| | | | | | | * Also copy CodeContractExtender in PrepareBoogieZip.bat * Added some comments and a new program in Test/textbook * Included refinement keywords in Chalice emacs mode * Used assignment instead of spec statement in DuplicatesVideo.chalice
* Boogie:Gravatar rustanleino2010-09-24
| | | | | * Added Test/textbook/DivMod.bpl, which embodies a conversion between C's div/mod operators and SMT Lib's div/mod operators. * Added a rudimentary printing of variables for captured states. It doesn't attempt to print everything at this time, and it doesn't work when variables get unique-ified by @@-suffixes. A more complete implementation will be added at a later time.
* Removed Output files. These are created on a local machine when the tests ↵Gravatar rustanleino2009-08-07
| | | | are run.
* Initial set of files.Gravatar mikebarnett2009-07-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 10:08:16 +0000