debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Fix some deprecation warnings from scalac 2.8.0.	kyessenov	2011-02-16
\| \| \| \| \|	Check for Boogie.exe only on Windows. Fix parser (_ is a keyword, not a delimiter)
*	Chalice: Applied patch 7685, this fixes a small bug that duplicated members ↵	alexanderjsummers	2011-01-12
\| \| \| \|	are not detected (neither duplicated methods, nor fields).
*	Applied patch 7636 - this fixes workitem 9978	alexanderjsummers	2011-01-12
\|
*	Chalice: this fixes a bug (an unsoundness) that arose in when a program ↵	mueller	2010-12-16
\| \| \| \|	combined predicates, read permissions to predicates, and forks.
*	Small changes to compile and test Chalice on Linux.	kyessenov	2010-12-04
\|
*	Chalice: white space delta in test file	rustanleino	2010-11-17
\| \| \| \|	Dafny: Simplified VSComp2010/Problem4-Queens.dfy from using an inductive ghost-method lemmas to just using an assert
*	Chalice: Automatically created a simple class diagram of the current AST	mschwerhoff	2010-11-13
\|
*	Chalice: Added axioms about div and mod. Updated DuplicatesVideo.chalice	rustanleino	2010-11-06
\|
*	Miscellaneous changes:	rustanleino	2010-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
*	Chalice: Now compiles with Scala 2.7.7 and 2.8.0, the latter yields many ↵	mschwerhoff	2010-10-21
\| \| \| \|	warnings, though. If 2.8.0 terminates with a stack overflow, increase stack size of the JVM (-Xss16M)
*	Chalice: allow replace by to match LocalVar	kyessenov	2010-10-09
\|
*	Chalice:	rustanleino	2010-10-09
\| \| \| \| \|	* extended the cheap type inference to also consider "in" expressions and quantifiers * added some refinement keywords to the Emacs mode for Chalice
*	Chalice: permit replaces by to match assign clauses	kyessenov	2010-10-09
\|
*	Chalice: fix a bug where output variables of a method were not decoupled.	kyessenov	2010-10-05
\|
*	Chalice: incorporate another regression test	kyessenov	2010-09-03
\|
*	Chalice: added Duplicates refinement from Verification Corner video	kyessenov	2010-09-02
\|
*	Chalice: fix in refinement loop target resolution; added "spec" as a keyword ↵	kyessenov	2010-09-02
\| \| \| \|	synonym to "var"
*	Chalice: working out mask transfers between concrete and abstract heaps -- ↵	kyessenov	2010-08-24
\| \| \| \|	next goal is to make this verify!
*	Chalice:	kyessenov	2010-08-24
\| \| \| \| \|	* fix bugs -- translateAssert and etran.fromPreGlobals were referring to globals by name instead of using current globals * example of finding duplicate elements in a sequence using a bitset
*	Chalice: exhale spec statement post condition in refinement block ↵	kyessenov	2010-08-23
\| \| \| \|	translation; tag global coupling assertions (bug fix)
*	Chalice: copy concrete values for every permission in coupling invariants of ↵	kyessenov	2010-08-23
\| \| \| \|	"this"
*	Chalice:	kyessenov	2010-08-23
\| \| \| \| \| \|	* added celebrity example (theory of sequences is still weak to prove basic things...) * bug in Chalice: old in while loops is ignored, needs to be fixed if ever want to complete DSW example * evil input from Z3 makes subsequent refinement proofs unsound; need to debug before building upon DSW.chalice; the error is triggered when adding parent field to Node
*	Chalice: spec stmt was unimplementable; changed it and refined; Z3 produces ↵	kyessenov	2010-08-22
\| \| \| \|	evil input again...
*	Chalice: start of a DSW refinement	kyessenov	2010-08-22
\|
*	Chalice: refining lists doesn't quite work yet...	kyessenov	2010-08-22
\|
*	Chalice: limited functions are still problematic (see Calculator.chalice)	kyessenov	2010-08-22
\|
*	Chalice:	kyessenov	2010-08-22
\| \| \| \|	* coupling invariants work (with certain restrictions as described in TODO comments)
*	Chalice:	kyessenov	2010-08-21
\| \| \| \| \|	* fix a compilation problem (scalac relied on old binaries) * combinator parser and state don't work well together -- added higher-order parser for method transform
*	server-side rename	kyessenov	2010-08-21
\|
*	Chalice: added syntax, printer and resolver for coupling invariants	kyessenov	2010-08-20
\|
*	VS 2010 mode for Chalice: some errors didn't show up in the window because ↵	kyessenov	2010-08-20
\| \| \| \|	positions were negative
*	Chalice: more regression tests; cosmetic changes to code	kyessenov	2010-08-19
\|
*	Chalice: added finite differencing refinement	kyessenov	2010-08-19
\|
*	Chalice:	kyessenov	2010-08-19
\| \| \| \| \|	* support multi-step refinement (convert refinement blocks into normal sequences of statements) * added tests
*	Chalice:	kyessenov	2010-08-19
\| \| \| \| \| \|	* added loop transform pattern * implemented translation of refined loops to Boogie (only assert new loop invariants) * refactored loop target computation code (async call was not handled as maybe some other statement)
*	Chalice: turn asserts into assumes for method refinements (use -noFreeAssume ↵	kyessenov	2010-08-19
\| \| \| \|	to disable)
*	Chalice:	kyessenov	2010-08-18
\| \| \| \| \| \|	* transforms are now callable * resolve transform specs * implement translation for refinement blocks (correct for manipulating locals, not globals)
*	Chalice:	kyessenov	2010-08-18
\| \| \| \| \| \| \|	* print type checked program (use -print -noTypecheck if you want old behavior) * refactored program context in Resolver ('errors' is kept as a ListBuffer and shared) * added resolver for refinement blocks (no loops yet) * pretty printer should work now for transforms
*	Chalice: added surface syntax for transform, AST matching algorithm	kyessenov	2010-08-17
\|
*	Chalice: refactored AST code for class hierarchy (no need for caches since ↵	kyessenov	2010-08-17
\| \| \| \|	Scala uses structural equality for case classes); landed first piece of refinement code
*	Chalice: bug fixes -- "check termination" flag was not properly preserved ↵	kyessenov	2010-08-16
\| \| \| \|	(i.e. if function app was inside old, the flag was ignored); != was not properly translated for sequences
*	Chalice: add pre-conditions to specification statements; semantically spec ↵	kyessenov	2010-08-13
\| \| \| \|	statement is just like a call statement now
*	Chalice: add specification statement ( ghost? (const\|var) (x (:T)?)+ [P(x)] )	kyessenov	2010-08-13
\|
*	Chalice: accept many input files at once; read from stdin if no input file ↵	kyessenov	2010-08-12
\| \| \| \|	specified
*	Chalice: example proving a simple identity (for refinement demonstration), ↵	kyessenov	2010-08-12
\| \| \| \|	revise code comments
*	Chalice: put classes and objects into package "chalice"	kyessenov	2010-08-11
\|
*	Chalice: fix "assume false" in the example (intended a spec statement)	kyessenov	2010-08-11
\|
*	Chalice: finite differences with recursion instead of loops	kyessenov	2010-08-10
\|
*	Chalice: added uninterpreted functions; attempting to re-verify Celebrity in ↵	kyessenov	2010-08-10
\| \| \| \|	Chalice
*	Chalice: forcefully kill Boogie with taskkill /T /F on termination	kyessenov	2010-08-10
\|