Proving Properties for Behavioural Specifications with Term Observation
Date
Authors
Berregeb,Narjes
Journal Title
Journal ISSN
Volume Title
Publisher
Journal of Universal Computer Science
Abstract
Description
Behavioural specifications allow to focus only on the"observable" behaviour of objects. These observations are made through "observable contexts" which are particular terms with a hole to be filled in with an object. We consider behavioural specifications based on the observation of a specified set of linear terms. The set of observable contexts is often infinite; therefore, we give an algorithm for computing some special contexts that we call "covering contexts", and show that they are sufficient for proving that two terms are behaviourally equal.
Keywords
behavioural specifications , term observation , observable contexts , covering contexts