Black-box specification in Spec
Abstract
This paper presents a language for giving black-box specifications in the early stages of software
design. The underlying computational model combines message passing with temporal events in a precisely
defined way. The features of the language, especially those important for large scale design are presented
by means of examples.