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