summaryrefslogtreecommitdiff
path: root/Binaries/DafnyPrelude.bpl
Commit message (Expand)AuthorAge
* Fixed axiom for Take/Update commuting.Gravatar Jason Koenig2011-07-19
* Strengthened axioms for multisets and sequences.Gravatar Jason Koenig2011-07-14
* Added multiset from sequence axioms, removed array range RHSs. Fixed issue wi...Gravatar Jason Koenig2011-07-13
* Multiset forming operators added.Gravatar Jason Koenig2011-07-11
* Partial implementation of multisets.Gravatar Jason Koenig2011-07-11
* Dafny: Dafny now uses the Euclidean definition of division. (Verifier and run...Gravatar Jason Koenig2011-07-08
* Dafny: Fixed axioms for Seq#Contains vs. the sequence building functionsGravatar Rustan Leino2011-06-29
* Dafny: fixed soundness problem with HeapSucc axiomGravatar Rustan Leino2011-06-01
* Dafny: To help verifications involving sequences of (boxed) booleans along, a...Gravatar Rustan Leino2011-05-16
* Dafny: added "choose" operator on setsGravatar rustanleino2011-03-26
* Dafny:Gravatar rustanleino2011-02-17
* Dafny: replaced the user-defined $ite function with Boogie's built-in if-then...Gravatar rustanleino2011-02-03
* Dafny: removed CEV instrumentationGravatar rustanleino2011-02-03
* Dafny: a partial first crack at a Dafny model-viewer provider, including capt...Gravatar rustanleino2010-11-01
* Dafny:Gravatar rustanleino2010-09-17
* Dafny:Gravatar rustanleino2010-09-14
* Dafny: added inlined functions making reads and updates of the heap explicitGravatar sboehme2010-08-27
* Dafny: Axiom about inverting a set union operation, similar to the recent on...Gravatar rustanleino2010-07-09
* Boogie:Gravatar rustanleino2010-06-22
* Dafny:Gravatar rustanleino2010-06-18
* Dafny:Gravatar rustanleino2010-05-21
* Dafny:Gravatar rustanleino2010-05-06
* Dafny:Gravatar rustanleino2010-03-31
* Dafny: Ensures that function axioms are not being used while their consisten...Gravatar rustanleino2010-03-19
* Dafny: Added if-then-else expressions (replacing and extending the previous b...Gravatar rustanleino2010-02-04
* Dafny: updated to reflect Boogie's new parsing of function argumentsGravatar rustanleino2010-01-07
* Added resolution and translation of algebraic datatypes and (in function bodi...Gravatar rustanleino2009-11-20
* Start (some parsing and resolution) of adding algebraic datatypes to Dafny.Gravatar rustanleino2009-11-08
* Added a sequence update expression in Dafny.Gravatar rustanleino2009-11-06
* Redesigned the encoding of Dafny generics, including the built-in types set a...Gravatar rustanleino2009-11-06
* Applied patch 4316, which fixes an unsoundness in the axiomatization of seque...Gravatar rustanleino2009-11-05
* Dafny: Added axioms for division and modulo.Gravatar rustanleino2009-09-15
* Dafny:Gravatar rustanleino2009-09-14
* Full (?) support in Dafny for Counterexample Visualizer predicates.Gravatar rustanleino2009-08-19
* Incorporated Counterexample Visualizer (CEV) information in the generated Boo...Gravatar rustanleino2009-08-15
* Initial set of files.Gravatar mikebarnett2009-07-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 14:39:50 +0000