SpEx-JML - Examples
This web page is a repository of source code for experiments and case studies we have carried out as part of several SpEx-JML projects.
1. Source code for experiments that show how JML can be chacked using Bogor (TACAS 2004)
- Replicated Workers (source, model)
- Bounded Buffer (source, model)
- Dining Philosophers (source, model)
- Linked Queue (source, model)
- Readers-Writers (source, model)
- Comparable Sort (source, model)
2. Source code for case studies on specifying multi-threaded programs with JML extended with concurrency constructs
- Bounded Buffer
- Dining Philosophers
- Linked Queue
- Readers-Writers
- java.util.Vector
- java.util.concurrent.ArrayBlockingQueue
- java.util.concurrent.ConcurrentLinkedQueue
- java.util.concurrent.CopyOnWriteArrayList
- java.util.concurrent.CopyOnWriteArraySet
- java.util.concurrent.DelayQueue
- java.util.concurrent.LinkedBlockingQueue
- java.util.concurrent.PriorityBlockingQueue
- java.util.concurrent.SynchronousQueue