Synchronisers: Semaphore

Verifying a semaphore. implemented in Java, that uses an atomic integer internally as synchroniser.

General information

ID150
Articlenone
Back-endChalice
LanguageJava
FeaturesAtomics, Loop invariants, Witnesses
Sources
Path to example filesynchronizers/Semaphore.java
Date2017-06-21

Statistical information

Lines of code99 lines (comments not included)
Lines of specification50 lines (50.51% of the total)
Computation time19169 milliseconds

Example code

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