Simply observable behavioral specification

Behavioral specifications are for specifying behavior of software or its components. We introduce a class of “sufficient” specifications “simply observable behavioral specifications”. In the process where we add conditional equations to a behavioral specification until we obtain a simply observable behavioral specification, we can find requirements for forgettable conditions. Verification methods of behavioral properties have difficulty when target systems are complex. Induction may be necessary. Finding lemmas may be necessary. However, by using a “sufficient” specification “a simply observable behavioral specification”, i.e. by capturing requirements sufficiently, the difficulty eases