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.