Collections Framework

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

November 25, 2009

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: