Collections Framework

Peter Lammich 🌐 with contributions from Andreas Lochbihler 🌐 and Thomas Tuerk

November 25, 2009

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

License

BSD License

History

April 25, 2012
New iterator foundation by Tuerk. Various maintenance changes.
October 10, 2011
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
December 1, 2010
New Interfaces: Priority Queues, Annotated Lists. Implemented by finger trees, (skew) binomial queues.
October 8, 2010
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.

Topics

Related publications

Session Collections

Session Collections_Examples

Depends on

Used by

Cite

× 
@article{Collections-AFP,
  author  = {Peter Lammich},
  title   = {Collections Framework},
  journal = {Archive of Formal Proofs},
  month   = {November},
  year    = {2009},
  note    = {\url{https://isa-afp.org/entries/Collections.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: