| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
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{https://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. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |