Collections Framework

 

Title: Collections Framework
Author: Peter Lammich
Contributors: Andreas Lochbihler and Thomas Tuerk
Submission date: 2009-11-25
Abstract: This development provides an efficient, extensible, machine checked collections framework. The library adopts the concepts of interface, implementation and generic algorithm from object-oriented programming and implements them in Isabelle/HOL. The framework features the use of data refinement techniques to refine an abstract specification (using high-level concepts like sets) to a more concrete implementation (using collection datastructures, like red-black-trees). The code-generator of Isabelle/HOL can be used to generate efficient code.
Change history: [2010-10-08]: New Interfaces: OrderedSet, OrderedMap, List. Fifo now implements list-interface: Function names changed: put/get --> enqueue/dequeue. New Implementations: ArrayList, ArrayHashMap, ArrayHashSet, TrieMap, TrieSet. Invariant-free datastructures: Invariant implicitely hidden in typedef. Record-interfaces: All operations of an interface encapsulated as record. Examples moved to examples subdirectory.
[2010-12-01]: New Interfaces: Priority Queues, Annotated Lists. Implemented by finger trees, (skew) binomial queues.
[2011-10-10]: SetSpec: Added operations: sng, isSng, bexists, size_abort, diff, filter, iterate_rule_insertP MapSpec: Added operations: sng, isSng, iterate_rule_insertP, bexists, size, size_abort, restrict, map_image_filter, map_value_image_filter Some maintenance changes
[2012-04-25]: New iterator foundation by Tuerk. Various maintenance changes.
[2012-08]: Collections V2. New features: Polymorphic iterators. Generic algorithm instantiation where required. Naming scheme changed from xx_opname to xx.opname. A compatibility file CollectionsV1 tries to simplify porting of existing theories, by providing old naming scheme and the old monomorphic iterator locales.
[2013-09]: Added Generic Collection Framework based on Autoref. The GenCF provides: Arbitrary nesting, full integration with Autoref.
[2014-06]: Maintenace changes to GenCF: Optimized inj_image on list_set. op_set_cart (Cartesian product). big-Union operation. atLeastLessThan - operation ({a..<b})
BibTeX:
@article{Collections-AFP,
  author  = {Peter Lammich},
  title   = {Collections Framework},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2009,
  note    = {\url{http://isa-afp.org/entries/Collections.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Automatic_Refinement, Binomial-Heaps, Finger-Trees, Native_Word, Refine_Monadic, Trie
Used by: Abstract_Completeness, CAVA_Automata, Containers, Datatype_Order_Generator, Deriving, DFS_Framework, Dijkstra_Shortest_Path, Formal_SSA, JinjaThreads, Ordinary_Differential_Equations, Refine_Imperative_HOL, Separation_Logic_Imperative_HOL, Transitive-Closure, Tree-Automata