JUCS - Journal of Universal Computer Science 12(10): 1413-1425, doi: 10.3217/jucs-012-10-1413
Proving Properties for Behavioural Specifications with Term Observation
expand article infoNarjes Berregeb
‡ Institut National des Sciences Appliquées et de Technologie, Tunisia
Open Access
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.
behavioural specifications, term observation, observable contexts, covering contexts