Abstract
Behavioral specifications are for specifying behavior of software or its components. In this paper, we introduce a class of "sufficient" specifications "simply observable behavioral specifications". In the process that 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 systems. Induction may be necessary. Finding lemmas may be necessary. But, by using a "sufficient" specification "a simply observable behavioral specification", i.e. by capturing requirements sufficiently, the difficulty eases.