### 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

- Computer science/Data structures

### Session Collections

- Sorted_List_Operations
- HashCode
- Code_Target_ICF
- SetIterator
- SetIteratorOperations
- Proper_Iterator
- It_to_It
- SetIteratorGA
- Gen_Iterator
- Idx_Iterator
- Iterator
- RBT_add
- Dlist_add
- Assoc_List
- Diff_Array
- Partial_Equivalence_Relation
- ICF_Tools
- Ord_Code_Preproc
- Record_Intf
- Locale_Code
- ICF_Spec_Base
- MapSpec
- Robdd
- Locale_Code_Ex
- DatRef
- SetAbstractionIterator
- GenCF_Chapter
- GenCF_Intf_Chapter
- Intf_Map
- Intf_Set
- Intf_Hash
- Intf_Comp
- GenCF_Gen_Chapter
- Gen_Set
- Gen_Map
- Gen_Map2Set
- Gen_Comp
- GenCF_Impl_Chapter
- Impl_Array_Stack
- Impl_List_Set
- Array_Iterator
- Impl_List_Map
- Impl_Array_Hash_Map
- Impl_RBT_Map
- Impl_Cfun_Set
- Impl_Array_Map
- Impl_Bit_Set
- Impl_Uv_Set
- Gen_Hash
- GenCF
- ICF_Chapter
- ICF_Spec_Chapter
- SetSpec
- ListSpec
- AnnotatedListSpec
- PrioSpec
- PrioUniqueSpec
- ICF_Gen_Algo_Chapter
- SetIteratorCollectionsGA
- MapGA
- SetGA
- SetByMap
- ListGA
- SetIndex
- Algos
- PrioByAnnotatedList
- PrioUniqueByAnnotatedList
- ICF_Impl_Chapter
- ListMapImpl
- ListMapImpl_Invar
- RBTMapImpl
- HashMap_Impl
- HashMap
- Trie_Impl
- Trie2
- TrieMapImpl
- ArrayHashMap_Impl
- ArrayHashMap
- ArrayMapImpl
- MapStdImpl
- ListSetImpl
- ListSetImpl_Invar
- ListSetImpl_NotDist
- ListSetImpl_Sorted
- RBTSetImpl
- HashSet
- TrieSetImpl
- ArrayHashSet
- ArraySetImpl
- SetStdImpl
- Fifo
- BinoPrioImpl
- SkewPrioImpl
- FTAnnotatedListImpl
- FTPrioImpl
- FTPrioUniqueImpl
- ICF_Impl
- ICF_Refine_Monadic
- ICF_Autoref
- ICF_Entrypoints_Chapter
- Collections
- CollectionsV1
- Collections_Entrypoints_Chapter
- Refine_Dflt
- Refine_Dflt_ICF
- Refine_Dflt_Only_ICF
- Userguides_Chapter
- Refine_Monadic_Userguide
- ICF_Userguide

### Session Collections_Examples

- Examples_Chapter
- Collection_Autoref_Examples_Chapter
- Succ_Graph
- Coll_Test
- Simple_DFS
- ICF_Test
- ICF_Only_Test
- Nested_DFS
- Combined_TwoSat
- Collection_Autoref_Examples
- Refine_Monadic_Examples_Chapter
- Bfs_Impl
- Foreach_Refine
- Refine_Fold
- Refine_Monadic_Examples
- ICF_Examples_Chapter
- itp_2010
- Exploration
- Exploration_DFS
- PerformanceTest
- ICF_Examples
- Collection_Examples

### Depends on

- Binomial Heaps and Skew Binomial Heaps
- Finger Trees
- Native Word
- Refinement for Monadic Programs
- Trie
- The CAVA Automata Library
- Light-weight Containers

### Used by

- Knuth–Morris–Pratt String Search
- Making Arbitrary Relational Calculus Queries Safe-Range
- A Sequent Calculus Prover for First-Order Logic with Functions
- Gale-Shapley Algorithm
- Kruskal’s Algorithm for Minimum Spanning Forest
- Transition Systems and Automata
- The Imperative Refinement Framework
- Algorithms for Reduced Ordered Binary Decision Diagrams
- Verified Construction of Static Single Assignment Form
- Deriving class instances for datatypes
- The CAVA Automata Library
- Abstract Completeness
- Light-weight Containers
- A Separation Logic Framework for Imperative HOL
- Ordinary Differential Equations
- Dijkstra’s Shortest Path Algorithm
- Executable Transitive Closures of Finite Relations
- Tree Automata
- Jinja with Threads

### Auto-related entries

- Verified Efficient Implementation of Gabow’s Strongly Connected Components Algorithm
- Automatic Data Refinement

## Cite

×

Collections-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Mar 2, 2013 : Isabelle2013
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 12, 2011 : Isabelle2011-1
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jun 30, 2010 : Isabelle2009-2
- Dec 13, 2009 : Isabelle2009-1
- Dec 12, 2009 : Isabelle2009-1
- Nov 29, 2009 : Isabelle2009