In the observer verification technique, to prove a behavioral property of a program
P, first, a program (O) representing the property must be designed.
This program listens all the input and output entries of P and
emits either
an