Probably the easiest way to define axioms for put() and get() is to treat
the binary semaphore s as a boolean variable and substitute for its
underlying value in predicates.
The get() axiom is
{ Q[ s <- false ] and s } <s.get()> { Q }
and the put() axiom is
{ Q[ s <- true ] } s.put() { Q }
Counting semaphores have a similar pair of axioms,
except the counting semaphore s represents a numeric instead of a boolean
value.
{ Q[ s <- s - 1 ] and s > 0 } <s.get()> { Q }
and the put() axiom is
{ Q[ s <- s + 1 ] } s.put() { Q }
This page last modified on 16 July 2003.