| Home |
| About |
| Submission Guidelines |
| Updating entries |
| Search |
| Index |
| Download |
project summary
Collections Framework
| Title: | Collections Framework |
| Author: | Peter Lammich, 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. |
| BibTeX: |
@article{Collections-AFP,
author = {Peter Lammich and Andreas Lochbihler and Thomas Tuerk},
title = {Collections Framework},
journal = {Archive of Formal Proofs},
month = nov,
year = 2009,
note = {\url{http://afp.sf.net/entries/Collections.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Binomial-Heaps, Finger-Trees |
| Status: [-STATUS-] | This is the development version, revision ae58066c3018, of this entry, generated for Isabelle revision 03034ba64679. The development version might change over time and is only permanently archived at Isabelle release points. It is provided as a preview of the next upcoming release. Please refer to release versions only in citations. If the status shows [FAIL], the links below will point to the last working version if any. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|