|
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: |
Binomial-Heaps, Finger-Trees, Native_Word, Refine_Monadic, Trie |
Used by: |
Abstract_Completeness, Containers, Deriving, Dijkstra_Shortest_Path, Formal_SSA, JinjaThreads, Kruskal, ROBDD, Separation_Logic_Imperative_HOL, Transition_Systems_and_Automata, Transitive-Closure, Tree-Automata |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|