Semaphore invariant

Given that:

S_initial >= 0

Invariant:

S_current = S_initial + #signal(S) - #wait(S)

#signal(S) -> no of signal() operations executed on S #wait(S) -> no of wait() operations completed on S

This is because each signal call always increments S by 1, wait call always decrements by 1.