| 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},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Binomial-Heaps, Finger-Trees |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|