Collections Framework

Peter Lammich with contributions from Andreas Lochbihler and Thomas Tuerk

25 November 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.
BSD License

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})

Depends On

Used by

Topics

Related Entries

Theories

Cite

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