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

Corresponding author: Narjes Berregeb ( narjes.benrajeb@topnet.tn )

© Narjes Berregeb.
This article is freely available under the J.UCS Open Content License.
Citation: Berregeb N (2006) Proving Properties for Behavioural Specifications with Term Observation. JUCS - Journal of Universal Computer Science 12(10): 1413-1425. https://doi.org/10.3217/jucs-012-10-1413
Open Access
Abstract
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