Teaching ADTs with the help of ConGu

This page includes some supporting material for using ConGu tool in a typical course on Algorithms and Data Structures that adopts Java. This material has been used in this course for several years.

For each ADT covered in the course, we provide:

• a formal specification of the ADT,
• a refinement mapping of the ADT into a Java implementation (to be completed by the students),
• a class that creates an instance of the ADT implementation and, then, randomly calls the ADTs operations (whenever they are guaranteed to be defined), a fixed number of times.

The ConGu tool, available in this Eclipse plug-in, checks at run-time that the provided implementation correctly implements the specified ADT. If you run the random class test under ConGu monitoring, ConGu will check if the implementation behaves as required by the specification.

See these lecture notes to learn more about the approach to the specification of ADTs and the runtime monitoring supported by ConGu.

Additional specifications, refinements and partial implementations, prepared for the course assignments, are available and will be provided on request (just drop me an email).

• BigNatural_ natural numbers + implementation with linked lists of digits
• FrequencyQueue_ frequency queues + implementation with a heap and a hash table
• LLSparseVector_ vector space + implementation with a linked list
• HTSparseVector_ vector space + implementation with a hash table
• VList_lists + implementation with linked list of vectors of growing size
• SEList_lists + implementation with doubly-linked circular list of blocks of fixed size
• TSTMap_maps with string keys + implementation with Ternary Search Tries

  Stacks | Queues | Dequeues | Binary Trees | Lists | Bags | Sorted Sets | Priority Queues | Maps

Stacks

• Specification 
• Java Implementation (with growing arrays) 
• Refinement
• StackRandomTest

Queues

• Specification 
• Java Implementation (with simply linked lists, to complete) 
• Refinement
• QueueRandomTest

Dequeues

• Specification 
• Java Implementation (with doubly linked lists, to complete) 
• Refinement
• DequeueRandomTest

Lists

• Specification 
• Java Implementation (with simply linked lists, to complete) 
• Refinement
• ListRandomTest

Binary Trees

• Specification 
• Java Implementation (immutable, with linked nodes, to complete) 
• Refinement
• BinaryTreeRandomTest

Bags

• Specification 
• Java Implementation 
• Refinement
• BagRandomTest

Sorted Sets

• Specification  (the module defines a core specification and a parameter specification)
• Java Implementation  (based on Binary Search Trees, making use of interface IOrderable)
• Refinement
• TreeSetRandomTest (this test class exercises, at the same time, a Bag of planets and other of integers; the file SortedSet.params defines that the tool will also check that classes Planet and MyInteger correctly implement a total order).

Priority Queues

• Specification  (the module defines a core specification and a parameter specification).
• Java Implementation  (with a heap, implementing interface MinPQ and using interface IPOrderable)
• Refinement
• HeapPriorityQueueRandomTest

Maps

• Specification  (the module defines a core specification and two parameter specifications for the key and value types).
• Java Implementation  (with a hash table using chaining)
• Refinement
• MapRandomTest

  Stacks | Queues | Dequeues | Binary Trees | Lists | Bags | Sorted Sets | Priority Queues | Maps