Single producer/consumer

Single producer and single-consumer verification using AtomicInteger. The contracts for the AtomicInteger is the version without magic-wand (delta).

General information

ID20
Articlenone
Back-endChalice
LanguageJava
FeaturesAtomics, Witnesses
Sources
Path to example fileatomics/RBProdCons.java
Date2017-06-15

Statistical information

Lines of code141 lines (comments not included)
Lines of specification59 lines (41.84% of the total)
Computation time19242 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.